begin
:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :
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 ComplLattStr 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 ComplLattStr holds L is join-associative
Lm3:
for L being non empty satisfying_DN_1 ComplLattStr holds L is Robbins
theorem Th58:
theorem Th59:
begin
:: deftheorem Def2 defines satisfying_MD_1 ROBBINS2:def 2 :
:: deftheorem Def3 defines satisfying_MD_2 ROBBINS2:def 3 :
Lm4:
now
let L be non
empty ComplLattStr ;
( 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
proof
let x,
y be
Element of
L;
(((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x
(((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) =
(((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` ))
by A3
.=
(((x ` ) + (((((y ` ) + x) ` ) + x) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` ))
by A3
.=
(y ` ) + x
by A20
;
hence
(((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x
;
verum
end;
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
proof
let x,
y be
Element of
L;
((x + y) ` ) + x = (y ` ) + x
set Y =
(y ` ) + x;
(y ` ) + x =
x + ((y ` ) + x)
by A29
.=
(((((y ` ) + x) ` ) + x) ` ) + x
by A3
.=
((x + y) ` ) + x
by A3
;
hence
((x + y) ` ) + x = (y ` ) + x
;
verum
end;
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
proof
let x,
y,
z be
Element of
L;
(x + y) + (y + z) = (x + y) + z
set Y =
x + y;
(x + y) + z =
(((z ` ) + (x + y)) ` ) + (x + y)
by A3
.=
(((z ` ) + (x + y)) ` ) + (y + (x + y))
by A10
.=
(x + y) + (y + z)
by A1, Def3
;
hence
(x + y) + (y + z) = (x + y) + z
;
verum
end;
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;