:: Formalization of Ortholattices via Orthoposets
:: by Adam Grabowski and Markus Moschner
::
:: Copyright (c) 2004-2019 Association of Mizar Users

:: Originally proved by McCune with the help of OTTER
definition
let L be non empty \/-SemiLattStr ;
attr L is join-Associative means :: ROBBINS3:def 1
for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);
end;

:: deftheorem defines join-Associative ROBBINS3:def 1 :
for L being non empty \/-SemiLattStr holds
( L is join-Associative iff for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) );

definition
let L be non empty /\-SemiLattStr ;
attr L is meet-Associative means :: ROBBINS3:def 2
for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);
end;

:: deftheorem defines meet-Associative ROBBINS3:def 2 :
for L being non empty /\-SemiLattStr holds
( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) );

definition
let L be non empty LattStr ;
attr L is meet-Absorbing means :: ROBBINS3:def 3
for x, y being Element of L holds x "\/" (x "/\" y) = x;
end;

:: deftheorem defines meet-Absorbing ROBBINS3:def 3 :
for L being non empty LattStr holds
( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x );

theorem Th1: :: ROBBINS3:1
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-idempotent & L is join-idempotent )
proof end;

theorem Th2: :: ROBBINS3:2
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-commutative & L is join-commutative )
proof end;

theorem Th3: :: ROBBINS3:3
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
L is meet-absorbing
proof end;

theorem Th4: :: ROBBINS3:4
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-associative & L is join-associative )
proof end;

theorem Th5: :: ROBBINS3:5
for L being non empty LattStr holds
( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
proof end;

registration
coherence
for b1 being non empty LattStr st b1 is Lattice-like holds
( b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing )
by Th5;
coherence
for b1 being non empty LattStr st b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing & b1 is join-absorbing holds
b1 is Lattice-like
by Th5;
end;

registration
coherence
for b1 being non empty PartialOrdered OrthoRelStr st b1 is OrderInvolutive holds
b1 is Dneg
proof end;
end;

theorem Th6: :: ROBBINS3:6
for L being non empty Dneg OrthoRelStr
for x being Element of L holds (x )  = x
proof end;

theorem Th7: :: ROBBINS3:7
for O being non empty PartialOrdered OrderInvolutive OrthoRelStr
for x, y being Element of O st x <= y holds
y  <= x
proof end;

registration
existence
ex b1 being PreOrthoPoset st
( b1 is with_infima & b1 is with_suprema & b1 is strict )
proof end;
end;

notation
let L be non empty \/-SemiLattStr ;
let x, y be Element of L;
synonym x |_| y for x "\/" y;
end;

notation
let L be non empty /\-SemiLattStr ;
let x, y be Element of L;
synonym x |^| y for x "/\" y;
end;

notation
let L be non empty RelStr ;
let x, y be Element of L;
synonym x "|^|" y for x "/\" y;
synonym x "|_|" y for x "\/" y;
end;

definition end;

definition end;

definition end;

definition
func TrivLattRelStr -> LattRelStr equals :: ROBBINS3:def 4
LattRelStr(# ,op2,op2,() #);
coherence
LattRelStr(# ,op2,op2,() #) is LattRelStr
;
end;

:: deftheorem defines TrivLattRelStr ROBBINS3:def 4 :
TrivLattRelStr = LattRelStr(# ,op2,op2,() #);

registration
coherence ;
end;

registration
existence
not for b1 being \/-SemiLattRelStr holds b1 is empty
proof end;
existence
not for b1 being /\-SemiLattRelStr holds b1 is empty
proof end;
cluster non empty for LattRelStr ;
existence
not for b1 being LattRelStr holds b1 is empty
proof end;
end;

theorem :: ROBBINS3:8
for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric & the InternalRel of R is transitive holds
( R is reflexive & R is antisymmetric & R is transitive )
proof end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being LattRelStr st
( b1 is antisymmetric & b1 is reflexive & b1 is transitive & b1 is with_suprema & b1 is with_infima )
proof end;
end;

registration
coherence ;
end;

Lm1:
;

registration
existence
ex b1 being non empty LattRelStr st b1 is Lattice-like
by Lm1;
end;

definition
let L be Lattice;
:: original: LattRel
redefine func LattRel L -> Order of the carrier of L;
coherence
LattRel L is Order of the carrier of L
proof end;
end;

definition end;

definition
func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5
OrthoLattRelStr(# ,op2,op2,(),op1 #);
coherence
OrthoLattRelStr(# ,op2,op2,(),op1 #) is OrthoLattRelStr
;
end;

:: deftheorem defines TrivCLRelStr ROBBINS3:def 5 :
TrivCLRelStr = OrthoLattRelStr(# ,op2,op2,(),op1 #);

:: Axiomatics for ortholattices is the classical one for lattices extended
:: by the three following:
:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1
:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific
:: x v c(x) = y v c(y). % ONE
definition
let L be non empty ComplStr ;
attr L is involutive means :Def6: :: ROBBINS3:def 6
for x being Element of L holds (x )  = x;
end;

:: deftheorem Def6 defines involutive ROBBINS3:def 6 :
for L being non empty ComplStr holds
( L is involutive iff for x being Element of L holds (x )  = x );

definition
let L be non empty ComplLLattStr ;
attr L is with_Top means :Def7: :: ROBBINS3:def 7
for x, y being Element of L holds x |_| (x ) = y |_| (y );
end;

:: deftheorem Def7 defines with_Top ROBBINS3:def 7 :
for L being non empty ComplLLattStr holds
( L is with_Top iff for x, y being Element of L holds x |_| (x ) = y |_| (y ) );

registration
coherence by STRUCT_0:def 10;
end;

registration
coherence ;
end;

registration
coherence
proof end;
end;

registration
coherence by STRUCT_0:def 10;
end;

registration
existence
ex b1 being 1 -element OrthoLattStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like )
proof end;
end;

definition end;

theorem Th9: :: ROBBINS3:9
for K, L being non empty LattStr 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 #) & K is join-commutative holds
L is join-commutative
proof end;

theorem Th10: :: ROBBINS3:10
for K, L being non empty LattStr 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 #) & K is meet-commutative holds
L is meet-commutative
proof end;

theorem Th11: :: ROBBINS3:11
for K, L being non empty LattStr 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 #) & K is join-associative holds
L is join-associative
proof end;

theorem Th12: :: ROBBINS3:12
for K, L being non empty LattStr 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 #) & K is meet-associative holds
L is meet-associative
proof end;

theorem Th13: :: ROBBINS3:13
for K, L being non empty LattStr 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 #) & K is join-absorbing holds
L is join-absorbing
proof end;

theorem Th14: :: ROBBINS3:14
for K, L being non empty LattStr 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 #) & K is meet-absorbing holds
L is meet-absorbing
proof end;

theorem :: ROBBINS3:15
for K, L being non empty LattStr 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 #) & K is Lattice-like holds
L is Lattice-like by ;

theorem :: ROBBINS3:16
for L1, L2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of L1, the L_join of L1 #) = \/-SemiLattStr(# the carrier of L2, the L_join of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "\/" b1 = a2 "\/" b2 ;

theorem :: ROBBINS3:17
for L1, L2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of L1, the L_meet of L1 #) = /\-SemiLattStr(# the carrier of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "/\" b1 = a2 "/\" b2 ;

theorem Th18: :: ROBBINS3:18
for K, L being non empty ComplStr
for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x  = y
proof end;

theorem Th19: :: ROBBINS3:19
for K, L being non empty ComplLLattStr st ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top holds
L is with_Top
proof end;

theorem Th20: :: ROBBINS3:20
for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan holds
L is de_Morgan
proof end;

theorem Th21: :: ROBBINS3:21
for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive holds
L is involutive
proof end;

definition
let R be RelStr ;
mode RelAugmentation of R -> LattRelStr means :: ROBBINS3:def 8
RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);
existence
ex b1 being LattRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #)
proof end;
end;

:: deftheorem defines RelAugmentation ROBBINS3:def 8 :
for R being RelStr
for b2 being LattRelStr holds
( b2 is RelAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) );

definition
let R be LattStr ;
mode LatAugmentation of R -> LattRelStr means :Def9: :: ROBBINS3:def 9
LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #);
existence
ex b1 being LattRelStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
proof end;
end;

:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :
for R being LattStr
for b2 being LattRelStr holds
( b2 is LatAugmentation of R iff LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) );

registration
let L be non empty LattStr ;
cluster -> non empty for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds not b1 is empty
proof end;
end;

registration
let L be non empty meet-associative LattStr ;
coherence
for b1 being LatAugmentation of L holds b1 is meet-associative
proof end;
end;

registration
let L be non empty join-associative LattStr ;
coherence
for b1 being LatAugmentation of L holds b1 is join-associative
proof end;
end;

registration
let L be non empty meet-commutative LattStr ;
coherence
for b1 being LatAugmentation of L holds b1 is meet-commutative
proof end;
end;

registration
let L be non empty join-commutative LattStr ;
coherence
for b1 being LatAugmentation of L holds b1 is join-commutative
proof end;
end;

registration
let L be non empty join-absorbing LattStr ;
cluster -> join-absorbing for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-absorbing
proof end;
end;

registration
let L be non empty meet-absorbing LattStr ;
cluster -> meet-absorbing for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-absorbing
proof end;
end;

definition
let L be non empty \/-SemiLattRelStr ;
attr L is naturally_sup-generated means :Def10: :: ROBBINS3:def 10
for x, y being Element of L holds
( x <= y iff x |_| y = y );
end;

:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def 10 :
for L being non empty \/-SemiLattRelStr holds
( L is naturally_sup-generated iff for x, y being Element of L holds
( x <= y iff x |_| y = y ) );

definition
let L be non empty /\-SemiLattRelStr ;
attr L is naturally_inf-generated means :: ROBBINS3:def 11
for x, y being Element of L holds
( x <= y iff x |^| y = x );
end;

:: deftheorem defines naturally_inf-generated ROBBINS3:def 11 :
for L being non empty /\-SemiLattRelStr holds
( L is naturally_inf-generated iff for x, y being Element of L holds
( x <= y iff x |^| y = x ) );

registration
let L be Lattice;
existence
ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

registration
existence
ex b1 being LattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof end;
end;

registration
existence
ex b1 being OrthoLattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof end;
end;

registration
existence
ex b1 being OrthoRelStr st
( b1 is 1 -element & b1 is reflexive )
proof end;
end;

registration
coherence
for b1 being 1 -element OrthoLattStr holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is well-complemented )
proof end;
end;

registration
coherence
for b1 being 1 -element reflexive OrthoRelStr holds
( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

registration
coherence
for b1 being 1 -element reflexive LattRelStr holds
( b1 is naturally_sup-generated & b1 is naturally_inf-generated )
proof end;
end;

registration
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is de_Morgan & b1 is Lattice-like & b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

registration
existence
ex b1 being non empty LattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

theorem Th22: :: ROBBINS3:22
for L being non empty naturally_sup-generated LattRelStr
for x, y being Element of L holds
( x <= y iff x [= y ) by Def10;

theorem Th23: :: ROBBINS3:23
for L being non empty Lattice-like naturally_sup-generated LattRelStr holds RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L
proof end;

registration
coherence
for b1 being non empty LattRelStr st b1 is naturally_sup-generated & b1 is Lattice-like holds
( b1 is with_infima & b1 is with_suprema )
proof end;
end;

definition
let R be OrthoLattStr ;
mode CLatAugmentation of R -> OrthoLattRelStr means :Def12: :: ROBBINS3:def 12
OrthoLattStr(# the carrier of it, the L_join of it, the L_meet of it, the Compl of it #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #);
existence
ex b1 being OrthoLattRelStr st OrthoLattStr(# the carrier of b1, the L_join of b1, the L_meet of b1, the Compl of b1 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)
proof end;
end;

:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
for R being OrthoLattStr
for b2 being OrthoLattRelStr holds
( b2 is CLatAugmentation of R iff OrthoLattStr(# the carrier of b2, the L_join of b2, the L_meet of b2, the Compl of b2 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) );

registration
let L be non empty OrthoLattStr ;
cluster -> non empty for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds not b1 is empty
proof end;
end;

registration
let L be non empty meet-associative OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-associative
proof end;
end;

registration
let L be non empty join-associative OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is join-associative
proof end;
end;

registration
let L be non empty meet-commutative OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-commutative
proof end;
end;

registration
let L be non empty join-commutative OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is join-commutative
proof end;
end;

registration
let L be non empty meet-absorbing OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-absorbing
proof end;
end;

registration
let L be non empty join-absorbing OrthoLattStr ;
coherence
for b1 being CLatAugmentation of L holds b1 is join-absorbing
proof end;
end;

registration
let L be non empty with_Top OrthoLattStr ;
cluster -> with_Top for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is with_Top
proof end;
end;

registration
let L be Ortholattice;
existence
ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

registration
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like & b1 is naturally_sup-generated & b1 is well-complemented )
proof end;
end;

theorem Th24: :: ROBBINS3:24
for L being non empty with_suprema with_infima PartialOrdered OrthoRelStr
for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )
proof end;

definition
let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original: |^|
redefine func a |^| b -> M3( the carrier of L);
commutativity
for a, b being Element of L holds a |^| b = b |^| a
by LATTICES:def 6;
end;

definition
let L be non empty join-commutative \/-SemiLattStr ;
let a, b be Element of L;
:: original: |_|
redefine func a |_| b -> M3( the carrier of L);
commutativity
for a, b being Element of L holds a |_| b = b |_| a
by LATTICES:def 4;
end;

registration
coherence
for b1 being non empty LattRelStr st b1 is meet-absorbing & b1 is join-absorbing & b1 is meet-commutative & b1 is naturally_sup-generated holds
b1 is reflexive
proof end;
end;

registration
coherence
for b1 being non empty LattRelStr st b1 is join-associative & b1 is naturally_sup-generated holds
b1 is transitive
proof end;
end;

registration
coherence
for b1 being non empty LattRelStr st b1 is join-commutative & b1 is naturally_sup-generated holds
b1 is antisymmetric
proof end;
end;

theorem Th25: :: ROBBINS3:25
for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|_|" y = x |_| y
proof end;

theorem Th26: :: ROBBINS3:26
for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|^|" y = x |^| y
proof end;

theorem :: ROBBINS3:27
proof end;

registration
let L be Ortholattice;
cluster -> involutive for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is involutive
proof end;
end;

registration
let L be Ortholattice;
cluster -> de_Morgan for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is de_Morgan
proof end;
end;

theorem Th28: :: ROBBINS3:28
for L being non empty OrthoLattRelStr st L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated holds
( L is Orthocomplemented & L is PartialOrdered )
proof end;

theorem :: ROBBINS3:29
for L being Ortholattice
for E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28;

registration
let L be Ortholattice;
coherence
for b1 being naturally_sup-generated CLatAugmentation of L holds b1 is Orthocomplemented
by Th28;
end;

theorem Th30: :: ROBBINS3:30
for L being non empty OrthoLattStr st L is Boolean & L is well-complemented & L is Lattice-like holds
L is Ortholattice
proof end;

registration
coherence
for b1 being non empty OrthoLattStr st b1 is Boolean & b1 is well-complemented & b1 is Lattice-like holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan )
by Th30;
end;