:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Copyright (c) 2008-2021 Association of Mizar Users

registration
let L be Lattice;
cluster LattStr(# the carrier of L, the L_join of L, the L_meet of L #) -> Lattice-like ;
coherence
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is Lattice-like
by ROBBINS3:15;
end;

theorem Th1: :: ROBBINS4:1
for K, L being Lattice st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds
LattPOSet K = LattPOSet L
proof end;

registration
coherence
for b1 being 1 -element OrthoLattStr holds b1 is meet-Absorbing
;
end;

registration
coherence
for b1 being Ortholattice holds b1 is lower-bounded
proof end;
coherence
for b1 being Ortholattice holds b1 is upper-bounded
proof end;
end;

theorem Th2: :: ROBBINS4:2
for L being Ortholattice
for a being Element of L holds
( a "\/" (a ) = Top L & a "/\" (a ) = Bottom L )
proof end;

theorem Th3: :: ROBBINS4:3
for L being non empty OrthoLattStr holds
( L is Ortholattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c ) "/\" (b )) ) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b )) ) ) )
proof end;

theorem Th4: :: ROBBINS4:4
for L being non empty Lattice-like involutive OrthoLattStr holds
( L is de_Morgan iff for a, b being Element of L st a [= b holds
b  [= a  )
proof end;

definition
let L be non empty OrthoLattStr ;
attr L is orthomodular means :Def1: :: ROBBINS4:def 1
for x, y being Element of L st x [= y holds
y = x "\/" ((x ) "/\" y);
end;

:: deftheorem Def1 defines orthomodular ROBBINS4:def 1 :
for L being non empty OrthoLattStr holds
( L is orthomodular iff for x, y being Element of L st x [= y holds
y = x "\/" ((x ) "/\" y) );

registration
existence
ex b1 being Ortholattice st
( b1 is trivial & b1 is orthomodular & b1 is modular & b1 is Boolean )
proof end;
end;

theorem Th5: :: ROBBINS4:5
for L being modular Ortholattice holds L is orthomodular
proof end;

definition end;

theorem Th6: :: ROBBINS4:6
for L being non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular OrthoLattStr
for x, y being Element of L holds x "\/" ((x ) "/\" (x "\/" y)) = x "\/" y by ;

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

:: deftheorem Def2 defines Orthomodular ROBBINS4:def 2 :
for L being non empty OrthoLattStr holds
( L is Orthomodular iff for x, y being Element of L holds x "\/" ((x ) "/\" (x "\/" y)) = x "\/" y );

registration
coherence
for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is Orthomodular holds
b1 is orthomodular
proof end;
coherence
for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is orthomodular holds
b1 is Orthomodular
by Th6;
end;

registration
coherence
for b1 being Ortholattice st b1 is modular holds
b1 is orthomodular
by Th5;
end;

registration
existence
ex b1 being Ortholattice st
( b1 is join-Associative & b1 is meet-Absorbing & b1 is de_Morgan & b1 is orthomodular )
proof end;
end;

definition
func B_6 -> RelStr equals :: ROBBINS4:def 3
InclPoset {0,1,(3 \ 1),2,(3 \ 2),3};
coherence
InclPoset {0,1,(3 \ 1),2,(3 \ 2),3} is RelStr
;
end;

:: deftheorem defines B_6 ROBBINS4:def 3 :
B_6 = InclPoset {0,1,(3 \ 1),2,(3 \ 2),3};

registration
cluster B_6 -> non empty ;
coherence
not B_6 is empty
;
coherence ;
end;

Lm1: 3 \ 2 misses 2
by XBOOLE_1:79;

Lm2:
by NAT_1:39;

then Lm3: 3 \ 2 misses 1
by ;

registration
coherence
proof end;
end;

theorem Th7: :: ROBBINS4:7
the carrier of () = {0,1,(3 \ 1),2,(3 \ 2),3}
proof end;

theorem Th8: :: ROBBINS4:8
for a being set st a in the carrier of () holds
a c= Segm 3
proof end;

definition
func Benzene -> strict OrthoLattStr means :Def4: :: ROBBINS4:def 4
( LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = latt B_6 & ( for x being Element of it
for y being Subset of 3 st x = y holds
the Compl of it . x = y  ) );
existence
ex b1 being strict OrthoLattStr st
( LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y  ) )
proof end;
uniqueness
for b1, b2 being strict OrthoLattStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y  ) & LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = latt B_6 & ( for x being Element of b2
for y being Subset of 3 st x = y holds
the Compl of b2 . x = y  ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :
for b1 being strict OrthoLattStr holds
( b1 = Benzene iff ( LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y  ) ) );

theorem Th9: :: ROBBINS4:9
the carrier of Benzene = {0,1,(3 \ 1),2,(3 \ 2),3}
proof end;

theorem Th10: :: ROBBINS4:10
the carrier of Benzene c= bool 3
proof end;

theorem Th11: :: ROBBINS4:11
for a being set st a in the carrier of Benzene holds
a c= {0,1,2} by ;

registration
coherence
not Benzene is empty
by Th9;
coherence
proof end;
end;

theorem Th12: :: ROBBINS4:12
LattPOSet LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = B_6
proof end;

theorem Th13: :: ROBBINS4:13
for a, b being Element of B_6
for x, y being Element of Benzene st a = x & b = y holds
( a <= b iff x [= y )
proof end;

theorem Th14: :: ROBBINS4:14
for a, b being Element of B_6
for x, y being Element of Benzene st a = x & b = y holds
( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
proof end;

theorem Th15: :: ROBBINS4:15
for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof end;

theorem Th16: :: ROBBINS4:16
for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof end;

theorem Th17: :: ROBBINS4:17
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof end;

theorem Th18: :: ROBBINS4:18
for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof end;

theorem Th19: :: ROBBINS4:19
for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof end;

theorem :: ROBBINS4:20
for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds
a "\/" b = 3
proof end;

theorem Th21: :: ROBBINS4:21
for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds
a "\/" b = 3
proof end;

theorem Th22: :: ROBBINS4:22
for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds
a "\/" b = 3
proof end;

theorem Th23: :: ROBBINS4:23
for a being Element of Benzene holds
( ( a = 0 implies a  = 3 ) & ( a = 3 implies a  = 0 ) & ( a = 1 implies a  = 3 \ 1 ) & ( a = 3 \ 1 implies a  = 1 ) & ( a = 2 implies a  = 3 \ 2 ) & ( a = 3 \ 2 implies a  = 2 ) )
proof end;

theorem Th24: :: ROBBINS4:24
for a, b being Element of Benzene holds
( a [= b iff a c= b )
proof end;

theorem Th25: :: ROBBINS4:25
for a, x being Element of Benzene st a = 0 holds
a "/\" x = a
proof end;

theorem Th26: :: ROBBINS4:26
for a, x being Element of Benzene st a = 0 holds
a "\/" x = x
proof end;

theorem Th27: :: ROBBINS4:27
for a, x being Element of Benzene st a = 3 holds
a "\/" x = a
proof end;

registration
coherence
proof end;
coherence
proof end;
end;

theorem :: ROBBINS4:28
proof end;

theorem Th29: :: ROBBINS4:29
proof end;

registration
coherence
proof end;
coherence
not Benzene is orthomodular
proof end;
end;

definition
let L be Ortholattice;
let a, b be Element of L;
pred a,b are_orthogonal means :: ROBBINS4:def 5
a [= b  ;
end;

:: deftheorem defines are_orthogonal ROBBINS4:def 5 :
for L being Ortholattice
for a, b being Element of L holds
( a,b are_orthogonal iff a [= b  );

notation
let L be Ortholattice;
let a, b be Element of L;
synonym a _|_ b for a,b are_orthogonal ;
end;

theorem :: ROBBINS4:30
for L being Ortholattice
for a being Element of L holds
( a _|_ a iff a = Bottom L )
proof end;

definition
let L be Ortholattice;
let a, b be Element of L;
:: original: are_orthogonal
redefine pred a,b are_orthogonal ;
symmetry
for a, b being Element of L st (L,b1,b2) holds
(L,b2,b1)
proof end;
end;

theorem :: ROBBINS4:31
for L being Ortholattice
for a, b, c being Element of L st a _|_ b & a _|_ c holds
( a _|_ b "/\" c & a _|_ b "\/" c )
proof end;

theorem :: ROBBINS4:32
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st b  [= a & a "/\" b = Bottom L holds
a = b  )
proof end;

theorem :: ROBBINS4:33
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b  )
proof end;

theorem Th34: :: ROBBINS4:34
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st b [= a holds
a "/\" ((a ) "\/" b) = b )
proof end;

theorem :: ROBBINS4:35
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L holds a "/\" ((a ) "\/" (a "/\" b)) = a "/\" b )
proof end;

theorem Th36: :: ROBBINS4:36
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a )) )
proof end;

theorem :: ROBBINS4:37
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a )) = (a "/\" b) "\/" (b "/\" (a )) )
proof end;

:: The short(est) axiomatization of orthomodular ortholattices
theorem :: ROBBINS4:38
for L being non empty OrthoLattStr holds
( L is Orthomodular_Lattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c ) "/\" (b )) ) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a )) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
proof end;

registration
coherence
for b1 being non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr holds b1 is with_Top
proof end;
end;

theorem :: ROBBINS4:39
for L being non empty OrthoLattStr holds
( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )
proof end;