:: 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 b₁ being non empty OrthoLattStr st b₁ is trivial holds
b₁ is meet-Absorbing ;

end;

registration

cluster non empty Lattice-like de_Morgan involutive with_Top -> lower-bounded OrthoLattStr ;
coherence
for b₁ being Ortholattice holds b₁ is lower-bounded

proof end;

cluster non empty Lattice-like de_Morgan involutive with_Top -> upper-bounded OrthoLattStr ;
coherence
for b₁ being Ortholattice holds b₁ 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 b₁ being Ortholattice st
( b₁ is trivial & b₁ is orthomodular & b₁ is modular & b₁ 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 b₁ being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b₁ is Orthomodular holds
b₁ 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 b₁ being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b₁ is orthomodular holds
b₁ is Orthomodular

proof end;

end;

registration

cluster non empty Lattice-like modular de_Morgan involutive with_Top -> orthomodular OrthoLattStr ;
coherence
for b₁ being Ortholattice st b₁ is modular holds
b₁ 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 b₁ being Ortholattice st
( b₁ is join-Associative & b₁ is meet-Absorbing & b₁ is de_Morgan & b₁ 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 b<sub>1</sub> being strict OrthoLattStr st
( LattStr(# the carrier of b<sub>1</sub>, the L_join of b<sub>1</sub>, the L_meet of b<sub>1</sub> #) = latt B_6 & ( for x being Element of b<sub>1</sub>
for y being Subset of 3 st x = y holds
the Compl of b<sub>1</sub> . x = y ` ) )

proof end;

uniqueness
for b₁, b₂ being strict OrthoLattStr st LattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁ #) = latt B_6 & ( for x being Element of b₁
for y being Subset of 3 st x = y holds
the Compl of b₁ . x = y ` ) & LattStr(# the carrier of b<sub>2</sub>, the L_join of b<sub>2</sub>, the L_meet of b<sub>2</sub> #) = latt B_6 & ( for x being Element of b<sub>2</sub>
for y being Subset of 3 st x = y holds
the Compl of b<sub>2</sub> . x = y ` ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :
for b₁ being strict OrthoLattStr holds
( b₁ = Benzene iff ( LattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁ #) = latt B_6 & ( for x being Element of b₁
for y being Subset of 3 st x = y holds
the Compl of b₁ . 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 b₁ being non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr holds b₁ 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;