:: by El\.zbieta M\c{a}dra and Adam Grabowski

::

:: Received June 27, 2008

:: Copyright (c) 2008-2019 Association of Mizar Users

registration

let L be Lattice;

coherence

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is Lattice-like by ROBBINS3:15;

end;
coherence

LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is Lattice-like by ROBBINS3:15;

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

LattPOSet K = LattPOSet L

proof end;

registration

coherence

for b_{1} being Ortholattice holds b_{1} is lower-bounded

for b_{1} being Ortholattice holds b_{1} is upper-bounded

end;
for b

proof end;

coherence for b

proof end;

theorem Th2: :: ROBBINS4:2

for L being Ortholattice

for a being Element of L holds

( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )

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 `)) ) ) )

( 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 ` )

( 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 ;

end;
attr L is orthomodular means :Def1: :: ROBBINS4:def 1

for x, y being Element of L st x [= y holds

y = x "\/" ((x `) "/\" y);

for x, y being Element of L st x [= y holds

y = x "\/" ((x `) "/\" y);

:: 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) );

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

ex b_{1} being Ortholattice st

( b_{1} is trivial & b_{1} is orthomodular & b_{1} is modular & b_{1} is Boolean )
end;

cluster non empty trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular lower-bounded upper-bounded V161() Boolean de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ;

existence ex b

( b

proof 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 LATTICES:5, Def1;

for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y by LATTICES:5, Def1;

definition

let L be non empty OrthoLattStr ;

end;
attr L is Orthomodular means :Def2: :: ROBBINS4:def 2

for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y;

for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y;

:: 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 );

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

for b_{1} being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b_{1} is Orthomodular holds

b_{1} is orthomodular

for b_{1} being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b_{1} is orthomodular holds

b_{1} is Orthomodular
by Th6;

end;

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 b

b

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 for OrthoLattStr ;

coherence for b

b

registration

for b_{1} being Ortholattice st b_{1} is modular holds

b_{1} is orthomodular
by Th5;

end;

cluster non empty Lattice-like modular de_Morgan involutive with_Top -> orthomodular for OrthoLattStr ;

coherence for b

b

registration

ex b_{1} being Ortholattice st

( b_{1} is join-Associative & b_{1} is meet-Absorbing & b_{1} is de_Morgan & b_{1} is orthomodular )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V161() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ;

existence ex b

( b

proof end;

registration

coherence

not B_6 is empty ;

coherence

( B_6 is reflexive & B_6 is transitive & B_6 is antisymmetric ) ;

end;
not B_6 is empty ;

coherence

( B_6 is reflexive & B_6 is transitive & B_6 is antisymmetric ) ;

Lm1: 3 \ 2 misses 2

by XBOOLE_1:79;

Lm2: Segm 1 c= Segm 2

by NAT_1:39;

then Lm3: 3 \ 2 misses 1

by Lm1, XBOOLE_1:63;

definition

ex b_{1} being strict OrthoLattStr st

( LattStr(# the carrier of b_{1}, the L_join of b_{1}, the L_meet of b_{1} #) = latt B_6 & ( for x being Element of b_{1}

for y being Subset of 3 st x = y holds

the Compl of b_{1} . x = y ` ) )

for b_{1}, b_{2} being strict OrthoLattStr st LattStr(# the carrier of b_{1}, the L_join of b_{1}, the L_meet of b_{1} #) = latt B_6 & ( for x being Element of b_{1}

for y being Subset of 3 st x = y holds

the Compl of b_{1} . x = y ` ) & LattStr(# the carrier of b_{2}, the L_join of b_{2}, the L_meet of b_{2} #) = latt B_6 & ( for x being Element of b_{2}

for y being Subset of 3 st x = y holds

the Compl of b_{2} . x = y ` ) holds

b_{1} = b_{2}
end;

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 ( 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 ` ) );

ex b

( LattStr(# the carrier of b

for y being Subset of 3 st x = y holds

the Compl of b

proof end;

uniqueness for b

for y being Subset of 3 st x = y holds

the Compl of b

for y being Subset of 3 st x = y holds

the Compl of b

b

proof end;

:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :

for b_{1} being strict OrthoLattStr holds

( b_{1} = Benzene iff ( LattStr(# the carrier of b_{1}, the L_join of b_{1}, the L_meet of b_{1} #) = latt B_6 & ( for x being Element of b_{1}

for y being Subset of 3 st x = y holds

the Compl of b_{1} . x = y ` ) ) );

for b

( b

for y being Subset of 3 st x = y holds

the Compl of b

registration
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 )

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 )

for x, y being Element of Benzene st a = x & b = y holds

( a "\/" b = x "\/" y & a "/\" b = x "/\" y )

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 ) )

( ( 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;

registration
end;

registration

coherence

( Benzene is involutive & Benzene is with_Top & Benzene is de_Morgan )

not Benzene is orthomodular

end;
( Benzene is involutive & Benzene is with_Top & Benzene is de_Morgan )

proof end;

coherence not Benzene is orthomodular

proof 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 ` );

for L being Ortholattice

for a, b being Element of L holds

( a,b are_orthogonal iff a [= b ` );

notation
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,b_{1},b_{2}) holds

(L,b_{2},b_{1})

end;
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,b

(L,b

proof 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 )

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 ` )

( 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 ` )

( 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 )

( 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 )

( 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 `)) )

( 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 `)) )

( 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 `)) ) ) )

( 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

for b_{1} being non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr holds b_{1} is with_Top
end;

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 b

proof 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 ) )

( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )

proof end;