:: Orthomodular Lattices :: by El\.zbieta M\c{a}dra and Adam Grabowski :: :: Received June 27, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, LATTICES, LATTICE3, SUBSET_1, FILTER_1, PBOOLE, EQREL_1, ZFMISC_1, ROBBINS3, XBOOLE_0, ROBBINS1, OPOSET_1, ORDERS_2, YELLOW_1, CARD_1, RELAT_2, TARSKI, STRUCT_0, XXREAL_0, FILTER_0, FUNCT_1, BINOP_1, RVSUM_1, SYMSP_1, ROBBINS4; notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, BINOP_1, FUNCT_1, ORDINAL1, CARD_1, NUMBERS, FUNCT_2, STRUCT_0, LATTICE3, LATTICES, ORDERS_2, ROBBINS1, YELLOW_1, ROBBINS3; constructors BINOP_1, REALSET2, LATTICE3, ROBBINS3, YELLOW_1, RELSET_1; registrations SUBSET_1, RELAT_1, STRUCT_0, LATTICES, YELLOW_1, ROBBINS1, SHEFFER1, ROBBINS3, XBOOLE_0, ORDINAL1; requirements SUBSET, BOOLE, NUMERALS, REAL; begin :: Preliminaries registration let L be Lattice; cluster the LattStr of L -> Lattice-like; end; theorem :: ROBBINS4:1 for K,L being Lattice st the LattStr of K = the LattStr of L holds LattPOSet K = LattPOSet L; registration cluster -> meet-Absorbing for 1-element OrthoLattStr; end; registration cluster -> lower-bounded for Ortholattice; cluster -> upper-bounded for Ortholattice; end; reserve L for Ortholattice, a, b, c for Element of L; theorem :: ROBBINS4:2 a "\/" a` = Top L & a "/\" a` = Bottom L; theorem :: 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`); theorem :: ROBBINS4:4 for L being involutive Lattice-like non empty OrthoLattStr holds L is de_Morgan iff for a,b being Element of L st a [= b holds b` [= a`; begin :: Orthomodularity definition let L be non empty OrthoLattStr; attr L is orthomodular means :: ROBBINS4:def 1 for x, y being Element of L st x [= y holds y = x "\/" (x` "/\" y); end; registration cluster trivial orthomodular modular Boolean for Ortholattice; end; theorem :: ROBBINS4:5 for L being modular Ortholattice holds L is orthomodular; definition mode Orthomodular_Lattice is orthomodular Ortholattice; end; theorem :: ROBBINS4:6 for L being orthomodular meet-absorbing join-absorbing join-associative meet-commutative non empty OrthoLattStr, x, y being Element of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y; definition let L be non empty OrthoLattStr; attr L is Orthomodular means :: ROBBINS4:def 2 for x, y being Element of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y; end; registration cluster Orthomodular -> orthomodular for meet-absorbing join-absorbing join-associative meet-commutative non empty OrthoLattStr; cluster orthomodular -> Orthomodular for meet-absorbing join-absorbing join-associative meet-commutative non empty OrthoLattStr; end; registration cluster modular -> orthomodular for Ortholattice; end; registration cluster join-Associative meet-Absorbing de_Morgan orthomodular for Ortholattice; end; begin :: Examples: The Benzene Ring definition func B_6 -> RelStr equals :: ROBBINS4:def 3 InclPoset { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }; end; registration cluster B_6 -> non empty; cluster B_6 -> reflexive transitive antisymmetric; end; registration cluster B_6 -> with_suprema with_infima; end; theorem :: ROBBINS4:7 the carrier of latt B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }; theorem :: ROBBINS4:8 for a being set st a in the carrier of latt B_6 holds a c= Segm 3; definition func Benzene -> strict OrthoLattStr means :: ROBBINS4:def 4 the LattStr of it = latt B_6 & for x being Element of it, y being Subset of 3 st x = y holds (the Compl of it).x = y`; end; theorem :: ROBBINS4:9 the carrier of Benzene = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }; theorem :: ROBBINS4:10 the carrier of Benzene c= bool 3; theorem :: ROBBINS4:11 for a being set st a in the carrier of Benzene holds a c= {0,1,2 }; registration cluster Benzene -> non empty; cluster Benzene -> Lattice-like; end; theorem :: ROBBINS4:12 LattPOSet the LattStr of Benzene = B_6; theorem :: ROBBINS4:13 for a, b being Element of B_6, x, y being Element of Benzene st a = x & b = y holds a <= b iff x [= y; theorem :: ROBBINS4:14 for a, b being Element of B_6, x, y being Element of Benzene st a = x & b = y holds a "\/" b = x "\/" y & a "/\" b = x "/\" y; theorem :: ROBBINS4:15 for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds a "\/" b = 3 & a "/\" b = 0; theorem :: ROBBINS4:16 for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds a "\/" b = 3 & a "/\" b = 0; theorem :: ROBBINS4:17 for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds a "\/" b = 3 & a "/\" b = 0; theorem :: ROBBINS4:18 for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds a "\/" b = 3 & a "/\" b = 0; theorem :: ROBBINS4:19 for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds a "\/" b = 3 & a "/\" b = 0; theorem :: ROBBINS4:20 for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds a "\/" b = 3; theorem :: ROBBINS4:21 for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds a "\/" b = 3; theorem :: ROBBINS4:22 for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds a "\/" b = 3; theorem :: 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); theorem :: ROBBINS4:24 for a, b being Element of Benzene holds a [= b iff a c= b; theorem :: ROBBINS4:25 for a, x being Element of Benzene st a = 0 holds a "/\" x = a; theorem :: ROBBINS4:26 for a, x being Element of Benzene st a = 0 holds a "\/" x = x; theorem :: ROBBINS4:27 for a, x being Element of Benzene st a = 3 holds a "\/" x = a; registration cluster Benzene -> lower-bounded; cluster Benzene -> upper-bounded; end; theorem :: ROBBINS4:28 Top Benzene = 3; theorem :: ROBBINS4:29 Bottom Benzene = 0; registration cluster Benzene -> involutive with_Top de_Morgan; cluster Benzene -> non orthomodular; end; begin :: Orthogonality definition let L be Ortholattice, a,b be Element of L; pred a, b are_orthogonal means :: ROBBINS4:def 5 a [= b`; end; notation let L be Ortholattice, a,b be Element of L; synonym a _|_ b for a, b are_orthogonal; end; theorem :: ROBBINS4:30 a _|_ a iff a = Bottom L; definition let L be Ortholattice; let a, b be Element of L; redefine pred a,b are_orthogonal; symmetry; end; theorem :: ROBBINS4:31 a _|_ b & a _|_ c implies a _|_ (b "/\" c) & a _|_ (b "\/" c); begin :: Orthomodularity Conditions theorem :: ROBBINS4:32 L is orthomodular iff for a,b being Element of L st b` [= a & a "/\" b = Bottom L holds a = b`; theorem :: ROBBINS4:33 L is orthomodular iff for a,b being Element of L st a _|_ b & a "\/" b = Top L holds a = b`; theorem :: ROBBINS4:34 L is orthomodular iff for a,b being Element of L st b [= a holds a "/\" (a` "\/" b) = b; theorem :: ROBBINS4:35 L is orthomodular iff for a,b holds a "/\" (a` "\/" (a "/\" b)) = a "/\" b; theorem :: ROBBINS4:36 L is orthomodular iff for a,b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" a`); theorem :: ROBBINS4:37 L is orthomodular iff for a,b st a [= b holds (a "\/" b) "/\" (b "\/" a`) = (a "/\" b) "\/" (b "/\" a`); ::$N 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`); reserve L for join-Associative meet-Absorbing de_Morgan orthomodular Lattice-like non empty OrthoLattStr; reserve v0,v1,v2,v64,v65 for Element of L; registration cluster -> with_Top for join-Associative meet-Absorbing de_Morgan orthomodular Lattice-like non empty OrthoLattStr; end; theorem :: ROBBINS4:39 for L being non empty OrthoLattStr holds L is Orthomodular_Lattice iff L is join-Associative meet-Absorbing de_Morgan Orthomodular;