:: On the Two Short Axiomatizations of Ortholattices
:: by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :
theorem Th1: :: ROBBINS2:1
theorem Th2: :: ROBBINS2:2
theorem Th3: :: ROBBINS2:3
theorem Th4: :: ROBBINS2:4
theorem Th5: :: ROBBINS2:5
theorem Th6: :: ROBBINS2:6
theorem Th7: :: ROBBINS2:7
theorem Th8: :: ROBBINS2:8
theorem Th9: :: ROBBINS2:9
theorem Th10: :: ROBBINS2:10
theorem Th11: :: ROBBINS2:11
theorem Th12: :: ROBBINS2:12
theorem Th13: :: ROBBINS2:13
theorem Th14: :: ROBBINS2:14
theorem Th15: :: ROBBINS2:15
theorem Th16: :: ROBBINS2:16
theorem Th17: :: ROBBINS2:17
theorem Th18: :: ROBBINS2:18
theorem Th19: :: ROBBINS2:19
theorem Th20: :: ROBBINS2:20
theorem Th21: :: ROBBINS2:21
theorem Th22: :: ROBBINS2:22
theorem Th23: :: ROBBINS2:23
theorem Th24: :: ROBBINS2:24
theorem Th25: :: ROBBINS2:25
theorem Th26: :: ROBBINS2:26
theorem Th27: :: ROBBINS2:27
Lm1:
for L being non empty satisfying_DN_1 ComplLattStr holds L is join-commutative
theorem Th28: :: ROBBINS2:28
theorem :: ROBBINS2:29
theorem :: ROBBINS2:30
theorem Th31: :: ROBBINS2:31
theorem Th32: :: ROBBINS2:32
theorem :: ROBBINS2:33
theorem Th34: :: ROBBINS2:34
theorem Th35: :: ROBBINS2:35
theorem Th36: :: ROBBINS2:36
theorem Th37: :: ROBBINS2:37
theorem Th38: :: ROBBINS2:38
theorem :: ROBBINS2:39
theorem Th40: :: ROBBINS2:40
theorem Th41: :: ROBBINS2:41
theorem Th42: :: ROBBINS2:42
theorem Th43: :: ROBBINS2:43
theorem Th44: :: ROBBINS2:44
theorem Th45: :: ROBBINS2:45
theorem Th46: :: ROBBINS2:46
theorem Th47: :: ROBBINS2:47
theorem Th48: :: ROBBINS2:48
theorem Th49: :: ROBBINS2:49
theorem Th50: :: ROBBINS2:50
theorem Th51: :: ROBBINS2:51
theorem Th52: :: ROBBINS2:52
theorem Th53: :: ROBBINS2:53
theorem :: ROBBINS2:54
theorem Th55: :: ROBBINS2:55
theorem :: ROBBINS2:56
theorem :: ROBBINS2:57
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: :: ROBBINS2:58
theorem Th59: :: ROBBINS2:59
:: 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 ;
:: thesis: ( 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 )
;
:: thesis: ( 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,
z being
Element of
L holds
(((((x ` ) + y) ` ) + z) ` ) + ((x ` ) + z) = z + ((x ` ) + y)
A4:
for
x,
y,
z being
Element of
L holds
(((x ` ) + y) ` ) + ((((x ` ) + z) ` ) + y) = y + x
A5:
for
x,
y,
z being
Element of
L holds
(((x ` ) + ((((y + x) ` ) + z) ` )) ` ) + (y + ((((y + x) ` ) + z) ` )) = y + x
A6:
for
x,
y being
Element of
L holds
(((x ` ) + y) ` ) + y = y + x
A8:
for
x,
y being
Element of
L holds
x + (y + (y + x)) = y + x
A9:
for
x,
y being
Element of
L holds
x + ((y ` ) + x) = (y ` ) + x
A10:
for
x being
Element of
L holds
x + x = x
A11:
for
x,
y being
Element of
L holds
x + (x + y) = x + y
A12:
for
x,
y being
Element of
L holds
(x + y) + y = x + y
A13:
for
x being
Element of
L holds
((x ` ) ` ) + x = x
A14:
for
x,
y being
Element of
L holds
x + (y + x) = y + x
A15:
for
x,
y being
Element of
L holds
x + (((x ` ) ` ) + y) = x + y
A16:
for
x,
y being
Element of
L holds
(x + y) + x = x + y
A17:
for
x,
y,
z being
Element of
L holds
(x + y) + (y + z) = (x + y) + z
A18:
for
x,
y being
Element of
L holds
((x + (y ` )) ` ) + y = y
A19:
for
x being
Element of
L holds
x + ((x ` ) ` ) = x
A20:
for
x,
y being
Element of
L holds
x + (((x ` ) + y) ` ) = x
A21:
for
x,
y being
Element of
L holds
x + ((y + (x ` )) ` ) = x
A22:
for
x,
y being
Element of
L holds
(((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x
A23:
for
x,
y being
Element of
L holds
((x + y) ` ) + x = (y ` ) + x
A24:
for
x,
y being
Element of
L holds
((x + y) ` ) + (((y ` ) + x) ` ) = (x ` ) + (((y ` ) + x) ` )
A25:
for
x being
Element of
L holds
x + ((((x ` ) ` ) ` ) ` ) = x
A26:
for
x being
Element of
L holds
((x ` ) ` ) ` = x `
A27:
for
x,
y being
Element of
L holds
x + ((y ` ) ` ) = x + y
A28:
for
x being
Element of
L holds
(x ` ) ` = x
A29:
for
x,
y being
Element of
L holds
(x ` ) + ((y + x) ` ) = x `
A30:
for
x,
y being
Element of
L holds
(x ` ) + ((x + y) ` ) = x `
A31:
for
x,
y being
Element of
L holds
x + (y ` ) = (y ` ) + x
A32:
for
x,
y being
Element of
L holds
x + y = y + x
hence
L is
join-commutative
by LATTICES:def 4;
:: thesis: ( L is Huntington & L is join-associative )
for
x,
y being
Element of
L holds
(((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x
hence
L is
Huntington
by ROBBINS1:def 6;
:: thesis: L is join-associative
for
x,
y,
z being
Element of
L holds
(x + y) + z = x + (y + z)
hence
L is
join-associative
by LATTICES:def 5;
:: thesis: verum
end;