begin
:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :
for L being non empty ComplLLattStr holds
( L is satisfying_DN_1 iff for x, y, z, u being Element of L holds (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z );
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
Lm1:
for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-commutative
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem
theorem
Lm2:
for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-associative
Lm3:
for L being non empty satisfying_DN_1 ComplLLattStr holds L is Robbins
theorem Th58:
theorem Th59:
begin
:: deftheorem Def2 defines satisfying_MD_1 ROBBINS2:def 2 :
for L being non empty ComplLLattStr holds
( L is satisfying_MD_1 iff for x, y being Element of L holds (((x `) + y) `) + x = x );
:: deftheorem Def3 defines satisfying_MD_2 ROBBINS2:def 3 :
for L being non empty ComplLLattStr holds
( L is satisfying_MD_2 iff for x, y, z being Element of L holds (((x `) + y) `) + (z + y) = y + (z + x) );
Lm4:
now
let L be non
empty ComplLLattStr ;
( L is satisfying_MD_1 & L is satisfying_MD_2 implies ( L is join-commutative & L is Huntington & L is join-associative ) )assume A1:
(
L is
satisfying_MD_1 &
L is
satisfying_MD_2 )
;
( L is join-commutative & L is Huntington & L is join-associative )A2:
for
x,
y being
Element of
L holds
(x `) + ((x `) + y) = (x `) + y
A3:
for
x,
y being
Element of
L holds
(((x `) + y) `) + y = y + x
A5:
for
x being
Element of
L holds
x + x = x
A6:
for
x,
y being
Element of
L holds
x + (x + y) = x + y
A7:
for
x,
y being
Element of
L holds
(x + y) + y = x + y
A8:
for
x,
y being
Element of
L holds
(x + y) + x = x + y
A9:
for
x,
y being
Element of
L holds
x + (y + (y + x)) = y + x
A10:
for
x,
y being
Element of
L holds
x + (y + x) = y + x
A11:
for
x,
y being
Element of
L holds
((x + (y `)) `) + y = y
A12:
for
x being
Element of
L holds
((x `) `) + x = x
A13:
for
x being
Element of
L holds
x + ((x `) `) = x
A14:
for
x,
y being
Element of
L holds
x + (((x `) `) + y) = x + y
A15:
for
x being
Element of
L holds
x + ((((x `) `) `) `) = x
A16:
for
x being
Element of
L holds
((x `) `) ` = x `
A17:
for
x,
y,
z being
Element of
L holds
(((x `) + y) `) + ((((x `) + z) `) + y) = y + x
A18:
for
x,
y being
Element of
L holds
x + ((y `) `) = x + y
A19:
for
x being
Element of
L holds
(x `) ` = x
A20:
for
x,
y,
z being
Element of
L holds
(((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x
A21:
for
x,
y being
Element of
L holds
(((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x
A22:
for
x,
y being
Element of
L holds
x + (((x `) + y) `) = x
A23:
for
x,
y being
Element of
L holds
(x `) + ((x + y) `) = x `
A24:
for
x,
y being
Element of
L holds
x + ((y + (x `)) `) = x
A25:
for
x,
y being
Element of
L holds
(x `) + ((y + x) `) = x `
A26:
for
x,
y being
Element of
L holds
x + (y `) = (y `) + x
A27:
for
x,
y being
Element of
L holds
x + y = y + x
hence
L is
join-commutative
by LATTICES:def 4;
( L is Huntington & L is join-associative )A28:
for
x,
y,
z being
Element of
L holds
(((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)
A29:
for
x,
y being
Element of
L holds
x + ((y `) + x) = (y `) + x
A30:
for
x,
y being
Element of
L holds
((x + y) `) + x = (y `) + x
A31:
for
x,
y being
Element of
L holds
((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `)
for
x,
y being
Element of
L holds
(((x `) + (y `)) `) + (((x `) + y) `) = x
hence
L is
Huntington
by ROBBINS1:def 6;
L is join-associative A32:
for
x,
y,
z being
Element of
L holds
(x + y) + (y + z) = (x + y) + z
for
x,
y,
z being
Element of
L holds
(x + y) + z = x + (y + z)
proof
let x,
y,
z be
Element of
L;
(x + y) + z = x + (y + z)
for
x,
y,
z being
Element of
L holds
(x + y) + (z + x) = y + (x + z)
then
(y + x) + (z + y) = x + (y + z)
;
then A33:
(x + y) + (z + y) = x + (y + z)
by A27;
(x + y) + z =
(x + y) + (y + z)
by A32
.=
x + (y + z)
by A27, A33
;
hence
(x + y) + z = x + (y + z)
;
verum
end;
hence
L is
join-associative
by LATTICES:def 5;
verum
end;