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


begin

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
cluster non empty trivial -> non empty meet-Absorbing OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is trivial holds
b1 is meet-Absorbing
;
end;

registration
cluster non empty Lattice-like de_Morgan involutive with_Top -> lower-bounded OrthoLattStr ;
coherence
for b1 being Ortholattice holds b1 is lower-bounded
proof end;
cluster non empty Lattice-like de_Morgan involutive with_Top -> upper-bounded OrthoLattStr ;
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;

begin

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
cluster non empty trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular lower-bounded upper-bounded V139() Boolean de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular OrthoLattStr ;
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
mode Orthomodular_Lattice is orthomodular Ortholattice;
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
proof end;

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
cluster non empty join-associative meet-commutative meet-absorbing join-absorbing Orthomodular -> non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular OrthoLattStr ;
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;
cluster non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular -> non empty join-associative meet-commutative meet-absorbing join-absorbing Orthomodular OrthoLattStr ;
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;
end;

registration
cluster non empty Lattice-like modular de_Morgan involutive with_Top -> orthomodular OrthoLattStr ;
coherence
for b1 being Ortholattice st b1 is modular holds
b1 is orthomodular
by Th5;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V139() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular OrthoLattStr ;
existence
ex b1 being Ortholattice st
( b1 is join-Associative & b1 is meet-Absorbing & b1 is de_Morgan & b1 is orthomodular )
proof end;
end;

begin

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
;
cluster B_6 -> reflexive transitive antisymmetric ;
coherence
( B_6 is reflexive & B_6 is transitive & B_6 is antisymmetric )
;
end;

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

Lm2: 1 c= 2
by NAT_1:40;

then Lm3: 3 \ 2 misses 1
by Lm1, XBOOLE_1:63;

registration
cluster B_6 -> with_suprema with_infima ;
coherence
( B_6 is with_suprema & B_6 is with_infima )
proof end;
end;

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

theorem Th8: :: ROBBINS4:8
for a being set st a in the carrier of (latt B_6) holds
a c= 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 Th10, CARD_1:89;

registration
cluster Benzene -> non empty strict ;
coherence
not Benzene is empty
by Th9;
cluster Benzene -> Lattice-like strict ;
coherence
Benzene is Lattice-like
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
cluster Benzene -> lower-bounded strict ;
coherence
Benzene is lower-bounded
proof end;
cluster Benzene -> upper-bounded strict ;
coherence
Benzene is upper-bounded
proof end;
end;

theorem :: ROBBINS4:28
Top Benzene = 3
proof end;

theorem Th29: :: ROBBINS4:29
Bottom Benzene = 0
proof end;

registration
cluster Benzene -> strict de_Morgan involutive with_Top ;
coherence
( Benzene is involutive & Benzene is with_Top & Benzene is de_Morgan )
proof end;
cluster Benzene -> strict non orthomodular ;
coherence
not Benzene is orthomodular
proof end;
end;

begin

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

:: deftheorem Def5 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 a,b are_orthogonal holds
b,a are_orthogonal
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;

begin

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;

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
cluster non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular -> non empty Lattice-like de_Morgan join-Associative meet-Absorbing with_Top orthomodular OrthoLattStr ;
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;