:: Orthomodular Lattices :: by El\.zbieta M\c{a}dra and Adam Grabowski :: :: Received June 27, 2008 :: Copyright (c) 2008-2012 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 proofend; registration cluster1 -element -> 1 -element meet-Absorbing for OrthoLattStr ; coherence for b1 being 1 -element OrthoLattStr holds b1 is meet-Absorbing ; end; registration cluster non empty Lattice-like de_Morgan involutive with_Top -> lower-bounded for OrthoLattStr ; coherence for b1 being Ortholattice holds b1 is lower-bounded proofend; cluster non empty Lattice-like de_Morgan involutive with_Top -> upper-bounded for OrthoLattStr ; coherence for b1 being Ortholattice holds b1 is upper-bounded proofend; end; theorem Th2: :: ROBBINS4:2 for L being Ortholattice for a being Element of L holds ( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L ) proofend; 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 `)) ) ) ) proofend; 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 ` ) proofend; begin definition let L be non empty OrthoLattStr ; attrL 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 V147() Boolean de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ; existence ex b1 being Ortholattice st ( b1 is trivial & b1 is orthomodular & b1 is modular & b1 is Boolean ) proofend; end; theorem Th5: :: ROBBINS4:5 for L being modular Ortholattice holds L is orthomodular proofend; 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 proofend; definition let L be non empty OrthoLattStr ; attrL 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 for OrthoLattStr ; coherence for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is Orthomodular holds b1 is orthomodular proofend; cluster non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular -> non empty join-associative meet-commutative meet-absorbing join-absorbing Orthomodular for OrthoLattStr ; coherence for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is orthomodular holds b1 is Orthomodular proofend; end; registration cluster non empty Lattice-like modular de_Morgan involutive with_Top -> orthomodular for 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 V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ; existence ex b1 being Ortholattice st ( b1 is join-Associative & b1 is meet-Absorbing & b1 is de_Morgan & b1 is orthomodular ) proofend; 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:39; 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 ) proofend; end; theorem Th7: :: ROBBINS4:7 the carrier of (latt B_6) = {0,1,(3 \ 1),2,(3 \ 2),3} proofend; theorem Th8: :: ROBBINS4:8 for a being set st a in the carrier of (latt B_6) holds a c= 3 proofend; 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 ` ) ) proofend; 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 proofend; 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} proofend; theorem Th10: :: ROBBINS4:10 the carrier of Benzene c= bool 3 proofend; 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:51; registration cluster Benzene -> non empty strict ; coherence not Benzene is empty by Th9; cluster Benzene -> Lattice-like strict ; coherence Benzene is Lattice-like proofend; end; theorem Th12: :: ROBBINS4:12 LattPOSet LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = B_6 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem Th19: :: ROBBINS4:19 for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds ( a "\/" b = 3 & a "/\" b = 0 ) proofend; theorem :: ROBBINS4:20 for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds a "\/" b = 3 proofend; theorem Th21: :: ROBBINS4:21 for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds a "\/" b = 3 proofend; theorem Th22: :: ROBBINS4:22 for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds a "\/" b = 3 proofend; 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 ) ) proofend; theorem Th24: :: ROBBINS4:24 for a, b being Element of Benzene holds ( a [= b iff a c= b ) proofend; theorem Th25: :: ROBBINS4:25 for a, x being Element of Benzene st a = 0 holds a "/\" x = a proofend; theorem Th26: :: ROBBINS4:26 for a, x being Element of Benzene st a = 0 holds a "\/" x = x proofend; theorem Th27: :: ROBBINS4:27 for a, x being Element of Benzene st a = 3 holds a "\/" x = a proofend; registration cluster Benzene -> lower-bounded strict ; coherence Benzene is lower-bounded proofend; cluster Benzene -> upper-bounded strict ; coherence Benzene is upper-bounded proofend; end; theorem :: ROBBINS4:28 Top Benzene = 3 proofend; theorem Th29: :: ROBBINS4:29 Bottom Benzene = 0 proofend; registration cluster Benzene -> strict de_Morgan involutive with_Top ; coherence ( Benzene is involutive & Benzene is with_Top & Benzene is de_Morgan ) proofend; cluster Benzene -> strict non orthomodular ; coherence not Benzene is orthomodular proofend; end; begin definition let L be Ortholattice; let a, b be Element of L; preda,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 ) proofend; definition let L be Ortholattice; let a, b be Element of L; :: original:are_orthogonal redefine preda,b are_orthogonal ; symmetry for a, b being Element of L st (L,b1,b2) holds (L,b2,b1) proofend; 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 ) proofend; 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 ` ) proofend; 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 ` ) proofend; 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 ) proofend; 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 ) proofend; 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 `)) ) proofend; 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 `)) ) proofend; :: [WP: ] 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 `)) ) ) ) proofend; 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 for OrthoLattStr ; coherence for b1 being non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr holds b1 is with_Top proofend; 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 ) ) proofend;