Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### Robbins Algebras vs. Boolean Algebras

by

Received June 12, 2001

MML identifier: ROBBINS1
[ Mizar article, MML identifier index ]

environ

vocabulary LATTICES, BINOP_1, BOOLE, MIDSP_1, VECTSP_2, REALSET1, SUBSET_1,
FUNCT_1, ARYTM_3, ARYTM_1, MIDSP_2, ROBBINS1;
notation TARSKI, XBOOLE_0, REALSET1, STRUCT_0, LATTICES, VECTSP_2, BINOP_1,
FUNCT_1, FUNCT_2, MIDSP_1;
constructors VECTSP_2, BINOP_1, LATTICES, REALSET1, MIDSP_2, PARTFUN1;
clusters STRUCT_0, RELSET_1, LATTICES, TEX_2, LATTICE2;

begin :: Preliminaries

definition
struct (1-sorted) ComplStr
(# carrier -> set,
Compl -> UnOp of the carrier #);
end;

definition
struct(\/-SemiLattStr, ComplStr) ComplLattStr
(# carrier -> set,
L_join -> BinOp of the carrier,
Compl -> UnOp of the carrier #);
end;

definition
struct (ComplLattStr, LattStr) OrthoLattStr
(# carrier -> set,
L_join, L_meet -> BinOp of the carrier,
Compl -> UnOp of the carrier #);
end;

definition
func TrivComplLat -> strict ComplLattStr equals
:: ROBBINS1:def 1
ComplLattStr (# {{}}, op2, op1 #);
end;

definition
func TrivOrtLat -> strict OrthoLattStr equals
:: ROBBINS1:def 2
OrthoLattStr (# {{}}, op2, op2, op1 #);
end;

definition
cluster TrivComplLat -> non empty trivial;

cluster TrivOrtLat -> non empty trivial;
end;

definition
cluster strict non empty trivial OrthoLattStr;

cluster strict non empty trivial ComplLattStr;
end;

definition let L be non empty trivial ComplLattStr;
cluster the ComplStr of L -> non empty trivial;
end;

definition
cluster strict non empty trivial ComplStr;
end;

definition let L be non empty ComplStr;
let x be Element of L;
func x -> Element of L equals
:: ROBBINS1:def 3
(the Compl of L).x;
end;

definition let L be non empty ComplLattStr,
x,y be Element of L;
redefine func x "\/" y;
synonym x + y;
end;

definition let L be non empty ComplLattStr;
let x,y be Element of L;
func x *' y -> Element of L equals
:: ROBBINS1:def 4
(x "\/" y);
end;

definition let L be non empty ComplLattStr;
attr L is Robbins means
:: ROBBINS1:def 5
for x, y being Element of L holds
((x + y) + (x + y)) = x;

attr L is Huntington means
:: ROBBINS1:def 6
for x, y being Element of L holds
(x + y) + (x + y) = x;
end;

definition let G be non empty \/-SemiLattStr;
attr G is join-idempotent means
:: ROBBINS1:def 7
for x being Element of G holds
x "\/" x = x;
end;

definition
cluster TrivComplLat -> join-commutative join-associative Robbins
Huntington join-idempotent;

cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins;
end;

definition
cluster TrivOrtLat -> meet-commutative meet-associative
meet-absorbing join-absorbing;
end;

definition
cluster strict join-associative join-commutative Robbins
join-idempotent Huntington (non empty ComplLattStr);
end;

definition
cluster strict Lattice-like Robbins Huntington (non empty OrthoLattStr);
end;

definition let L be join-commutative (non empty ComplLattStr),
x,y be Element of L;
redefine func x + y;
commutativity;
end;

theorem :: ROBBINS1:1  :: 4.8
for L being Huntington join-commutative join-associative
(non empty ComplLattStr),
a, b being Element of L holds
(a *' b) + (a *' b) = a;

theorem :: ROBBINS1:2  :: 4.9
for L being Huntington join-commutative join-associative
(non empty ComplLattStr),
a being Element of L holds
a + a = a + a;

theorem :: ROBBINS1:3  :: 4.10
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
x being Element of L holds
x = x;

theorem :: ROBBINS1:4  :: 4.11 revised p. 557 without idempotency
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L holds
a + a = b + b;

theorem :: ROBBINS1:5  :: 4.12
for L being join-commutative join-associative join-idempotent Huntington
(non empty ComplLattStr)
ex c being Element of L st
for a being Element of L holds c + a = c & a + a = c;

theorem :: ROBBINS1:6  :: 4.12
for L being join-commutative join-associative join-idempotent Huntington
(non empty ComplLattStr) holds
L is upper-bounded;

definition
cluster join-commutative join-associative join-idempotent Huntington
-> upper-bounded (non empty ComplLattStr);
end;

definition let L be join-commutative join-associative join-idempotent
Huntington (non empty ComplLattStr);
redefine func Top L means
:: ROBBINS1:def 8
ex a being Element of L st
it = a + a;
end;

theorem :: ROBBINS1:7  :: 4.13
for L being join-commutative join-associative join-idempotent Huntington
(non empty ComplLattStr)
ex c being Element of L st
for a being Element of L holds c *' a = c & (a + a) = c;

theorem :: ROBBINS1:8  :: 4.18
for L being join-commutative join-associative (non empty ComplLattStr),
a, b being Element of L holds
a *' b = b *' a;

definition let L be join-commutative join-associative (non empty ComplLattStr);
let x,y be Element of L;
redefine func x *' y;
commutativity;
end;

definition let L be join-commutative join-associative join-idempotent
Huntington (non empty ComplLattStr);
func Bot L -> Element of L means
:: ROBBINS1:def 9
for a being Element of L holds it *' a = it;
end;

theorem :: ROBBINS1:9
for L being join-commutative join-associative join-idempotent Huntington
(non empty ComplLattStr),
a being Element of L holds
Bot L = (a + a);

theorem :: ROBBINS1:10
for L being join-commutative join-associative join-idempotent Huntington
(non empty ComplLattStr) holds
(Top L) = Bot L & Top L = (Bot L);

theorem :: ROBBINS1:11  :: 4.14
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L st
a = b holds a = b;

theorem :: ROBBINS1:12  :: 4.15 proof without join-idempotency, no top at all
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L holds
a + (b + b) = a;

theorem :: ROBBINS1:13  :: 4.5
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a + a = a;

definition
cluster join-commutative join-associative Huntington ->
join-idempotent (non empty ComplLattStr);
end;

theorem :: ROBBINS1:14  :: 4.15
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a + Bot L = a;

theorem :: ROBBINS1:15 :: 4.16
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a *' Top L = a;

theorem :: ROBBINS1:16  :: 4.17
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a *' a = Bot L;

theorem :: ROBBINS1:17  :: 4.19
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
a *' (b *' c) = a *' b *' c;

theorem :: ROBBINS1:18  :: 4.20
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L holds
a + b = (a *' b);

theorem :: ROBBINS1:19 :: 4.21
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a *' a = a;

theorem :: ROBBINS1:20 :: 4.22
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a being Element of L holds
a + Top L = Top L;

theorem :: ROBBINS1:21  :: 4.24
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L holds
a + (a *' b) = a;

theorem :: ROBBINS1:22  :: 4.25
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L holds
a *' (a + b) = a;

theorem :: ROBBINS1:23  :: 4.26
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L st
a + b = Top L & b + a = Top L holds a = b;

theorem :: ROBBINS1:24  :: 4.27
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b being Element of L st
a + b = Top L & a *' b = Bot L holds a = b;

theorem :: ROBBINS1:25  :: 4.28
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
(a *' b *' c) + (a *' b *' c) + (a *' b *' c) +
(a *' b *' c) + (a *' b *' c) + (a *' b *' c) +
(a *' b *' c) + (a *' b *' c) = Top L;

theorem :: ROBBINS1:26  :: 4.29
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
(a *' c) *' (b *' c) = Bot L &
(a *' b *' c) *' (a *' b *' c) = Bot L &
(a *' b *' c) *' (a *' b *' c) = Bot L &
(a *' b *' c) *' (a *' b *' c) = Bot L &
(a *' b *' c) *' (a *' b *' c) = Bot L &
(a *' b *' c) *' (a *' b *' c) = Bot L;

theorem :: ROBBINS1:27  :: 4.30
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
(a *' b) + (a *' c) = (a *' b *' c) + (a *' b *' c) + (a *' b *' c);

theorem :: ROBBINS1:28  :: 4.31
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
(a *' (b + c)) = (a *' b *' c) + (a *' b *' c) + (a *' b *' c)
+ (a *' b *' c) + (a *' b *' c);

theorem :: ROBBINS1:29  :: 4.32
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
((a *' b) + (a *' c)) + (a *' (b + c)) = Top L;

theorem :: ROBBINS1:30   :: 4.33
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
((a *' b) + (a *' c)) *' (a *' (b + c)) = Bot L;

theorem :: ROBBINS1:31  :: 4.34
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
a *' (b + c) = (a *' b) + (a *' c);

theorem :: ROBBINS1:32 :: 4.35
for L being join-commutative join-associative Huntington
(non empty ComplLattStr),
a, b, c being Element of L holds
a + (b *' c) = (a + b) *' (a + c);

begin :: Pre-Ortholattices

definition let L be non empty OrthoLattStr;
attr L is well-complemented means
:: ROBBINS1:def 10
for a being Element of L holds
a is_a_complement_of a;
end;

definition
cluster TrivOrtLat -> Boolean well-complemented;
end;

definition
mode preOrthoLattice is Lattice-like (non empty OrthoLattStr);
end;

definition
cluster strict Boolean well-complemented preOrthoLattice;
end;

theorem :: ROBBINS1:33
for L being distributive well-complemented preOrthoLattice,
x being Element of L
holds x = x;

theorem :: ROBBINS1:34
for L being bounded distributive well-complemented preOrthoLattice,
x, y being Element of L
holds x "/\" y = (x "\/" y);

begin :: Correspondence between boolean preOrthoLattice and boolean lattice
:: according to the definition given in \cite{LATTICES.ABS}

definition let L be non empty ComplLattStr;
func CLatt L -> strict OrthoLattStr means
:: ROBBINS1:def 11
the carrier of it = the carrier of L &
the L_join of it = the L_join of L &
the Compl of it = the Compl of L &
for a, b being Element of L holds
(the L_meet of it).(a,b) = a *' b;
end;

definition let L be non empty ComplLattStr;
cluster CLatt L -> non empty;
end;

definition let L be join-commutative (non empty ComplLattStr);
cluster CLatt L -> join-commutative;
end;

definition let L be join-associative (non empty ComplLattStr);
cluster CLatt L -> join-associative;
end;

definition let L be join-commutative join-associative (non empty ComplLattStr);
cluster CLatt L -> meet-commutative;
end;

theorem :: ROBBINS1:35
for L being non empty ComplLattStr,
a, b being Element of L,
a', b' being Element of CLatt L st
a = a' & b = b' holds a *' b = a' "/\" b' & a + b = a' "\/" b' & a = a';

definition let L be join-commutative join-associative Huntington
(non empty ComplLattStr);
cluster CLatt L -> meet-associative join-absorbing meet-absorbing;
end;

definition let L be Huntington (non empty ComplLattStr);
cluster CLatt L -> Huntington;
end;

definition let L be join-commutative join-associative Huntington
(non empty ComplLattStr);
cluster CLatt L -> lower-bounded;
end;

theorem :: ROBBINS1:36
for L being join-commutative join-associative Huntington
(non empty ComplLattStr) holds
Bot L = Bottom CLatt L;

definition let L be join-commutative join-associative Huntington
(non empty ComplLattStr);
cluster CLatt L -> complemented distributive bounded;
end;

begin :: Proofs according to Bernd Ingo Dahn

definition let G be non empty ComplLattStr,
x be Element of G;
redefine func x;
synonym -x;
end;

definition let G be join-commutative (non empty ComplLattStr);
redefine attr G is Huntington means
:: ROBBINS1:def 12
for x, y being Element of G holds
-(-x + -y) + -(x + -y) = y;
end;

definition let G be non empty ComplLattStr;
attr G is with_idempotent_element means
:: ROBBINS1:def 13
ex x being Element of G st x + x = x;
end;

reserve G for Robbins join-associative join-commutative
(non empty ComplLattStr);
reserve x, y, z, u, v for Element of G;

definition let G be non empty ComplLattStr,
x, y be Element of G;
func \delta (x, y) -> Element of G equals
:: ROBBINS1:def 14
-(-x + y);
end;

definition let G be non empty ComplLattStr,
x, y be Element of G;
func Expand (x, y) -> Element of G equals
:: ROBBINS1:def 15
\delta (x + y, \delta(x, y));
end;

definition let G be non empty ComplLattStr,
x be Element of G;
func x _0 -> Element of G equals
:: ROBBINS1:def 16
-(-x + x);

func Double x -> Element of G equals
:: ROBBINS1:def 17
x + x;
end;

definition let G be non empty ComplLattStr,
x be Element of G;
func x _1 -> Element of G equals
:: ROBBINS1:def 18
x _0 + x;
func x _2 -> Element of G equals
:: ROBBINS1:def 19
x _0 + Double x;
func x _3 -> Element of G equals
:: ROBBINS1:def 20
x _0 + (Double x + x);
func x _4 -> Element of G equals
:: ROBBINS1:def 21
x _0 + (Double x + Double x);
end;

theorem :: ROBBINS1:37
\delta ((x + y), (\delta (x, y))) = y;

theorem :: ROBBINS1:38
Expand (x, y) = y;

theorem :: ROBBINS1:39
\delta (-x + y, z) = -(\delta (x, y) + z);

theorem :: ROBBINS1:40
\delta (x, x) = x _0;

theorem :: ROBBINS1:41
\delta (Double x, x _0) = x;

theorem :: ROBBINS1:42  :: Lemma 1
\delta (x _2, x) = x _0;

theorem :: ROBBINS1:43
x _2 + x = x _3;

theorem :: ROBBINS1:44
x _4 + x _0 = x _3 + x _1;

theorem :: ROBBINS1:45
x _3 + x _0 = x _2 + x _1;

theorem :: ROBBINS1:46
x _3 + x = x _4;

theorem :: ROBBINS1:47  :: Lemma 2
\delta (x _3, x _0) = x;

theorem :: ROBBINS1:48   :: Left Argument Substitution
-x = -y implies \delta (x, z) = \delta (y,z);

theorem :: ROBBINS1:49  :: Exchange
\delta (x, -y) = \delta (y, -x);

theorem :: ROBBINS1:50  :: Lemma 3
\delta (x _3, x) = x _0;

theorem :: ROBBINS1:51  :: Lemma 4
\delta (x _1 + x _3, x) = x _0;

theorem :: ROBBINS1:52  :: Lemma 5
\delta (x _1 + x _2, x) = x _0;

theorem :: ROBBINS1:53  :: Lemma 6
\delta (x _1 + x _3, x _0) = x;

definition let G, x;
func \beta x -> Element of G equals
:: ROBBINS1:def 22
-(x _1 + x _3) + x + -(x _3);
end;

theorem :: ROBBINS1:54  :: Lemma 7
\delta (\beta x, x) = -x _3;

theorem :: ROBBINS1:55  :: Lemma 8
\delta (\beta x, x) = -(x _1 + x _3);

theorem :: ROBBINS1:56 :: Winker Second Condition
ex y, z st -(y + z) = -z;

begin :: Proofs according to Bill McCune

theorem :: ROBBINS1:57
(for z holds --z = z) implies G is Huntington;

theorem :: ROBBINS1:58
G is with_idempotent_element implies G is Huntington;

definition
cluster TrivComplLat -> with_idempotent_element;
end;

definition
cluster with_idempotent_element ->
Huntington (Robbins join-associative join-commutative
(non empty ComplLattStr));
end;

theorem :: ROBBINS1:59
(ex c, d being Element of G st c + d = c) implies
G is Huntington;

theorem :: ROBBINS1:60
ex y, z st y + z = z;

definition
cluster Robbins -> Huntington (join-associative join-commutative
(non empty ComplLattStr));
end;

definition let L be non empty OrthoLattStr;
attr L is de_Morgan means
:: ROBBINS1:def 23
for x, y being Element of L holds x "/\" y = (x "\/" y);
end;

definition let L be non empty ComplLattStr;
cluster CLatt L -> de_Morgan;
end;

theorem :: ROBBINS1:61
for L being well-complemented join-commutative meet-commutative
(non empty OrthoLattStr),
x being Element of L holds
x + x = Top L & x "/\" x = Bottom L;

theorem :: ROBBINS1:62
for L being bounded distributive well-complemented preOrthoLattice holds
(Top L) = Bottom L;

definition
cluster TrivOrtLat -> de_Morgan;
end;

definition
cluster strict de_Morgan Boolean Robbins Huntington preOrthoLattice;
end;

definition
cluster join-associative join-commutative de_Morgan ->
meet-commutative (non empty OrthoLattStr);
end;

theorem :: ROBBINS1:63
for L being Huntington de_Morgan preOrthoLattice holds
Bot L = Bottom L;

definition
cluster Boolean -> Huntington (well-complemented preOrthoLattice);
end;

definition
cluster Huntington -> Boolean (de_Morgan preOrthoLattice);
end;

definition
cluster Robbins de_Morgan -> Boolean preOrthoLattice;

cluster Boolean -> Robbins (well-complemented preOrthoLattice);
end;

`