:: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander
:: by Adam Grabowski and Damian Sawicki
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


definition
let L be non empty LattStr ;
attr L is satisfying_Sholander_1 means :: ROBBINS5:def 1
 for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0);
end;

:: deftheorem defines satisfying_Sholander_1 ROBBINS5:def 1 :
for L being non empty LattStr holds
( L is satisfying_Sholander_1 iff for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) );

theorem Lemma1: :: ROBBINS5:1
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0 being Element of L holds v0 "/\" v0 = v0
proof end;

theorem JoinIdem: :: ROBBINS5:2
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0 being Element of L holds v0 "\/" v0 = v0
proof end;

:: Proofs
theorem MeetCom: :: ROBBINS5:3
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0
proof end;

:: Join-commutativity
theorem JoinCom: :: ROBBINS5:4
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0
proof end;

:: Meet-associativity
theorem MeetAssoc: :: ROBBINS5:5
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2)
proof end;

:: Third
theorem :: ROBBINS5:6
for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) holds
for v0, v1 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ;

:: Sixth
theorem MeetAbsor: :: ROBBINS5:7
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0
proof end;

:: Join-associativity
theorem JoinAssoc: :: ROBBINS5:8
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2)
proof end;

:: Seventh file
theorem Seventh: :: ROBBINS5:9
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)
proof end;

:: Eighth File
theorem :: ROBBINS5:10
for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1, v2 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2)
proof end;

theorem LatToSho: :: ROBBINS5:11
for L being non empty join-commutative meet-commutative distributive LattStr
for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) by LATTICES:def 11;

theorem Combined: :: ROBBINS5:12
for L being non empty LattStr holds
( L is distributive Lattice iff ( L is join-absorbing & L is satisfying_Sholander_1 ) )
proof end;

registration
cluster non empty join-absorbing satisfying_Sholander_1 -> non empty Lattice-like distributive for LattStr ;
coherence
for b1 being non empty LattStr st b1 is join-absorbing & b1 is satisfying_Sholander_1 holds
( b1 is distributive & b1 is Lattice-like ) by Combined;
cluster non empty join-commutative meet-commutative distributive -> non empty satisfying_Sholander_1 for LattStr ;
coherence
for b1 being non empty LattStr st b1 is distributive & b1 is join-commutative & b1 is meet-commutative holds
b1 is satisfying_Sholander_1 by LatToSho;
end;

definition
let L be non empty LattStr ;
attr L is satisfying_McKenzie_1 means :: ROBBINS5:def 2
 for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0;
attr L is satisfying_McKenzie_2 means :: ROBBINS5:def 3
 for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0;
attr L is satisfying_McKenzie_3 means :: ROBBINS5:def 4
 for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1;
attr L is satisfying_McKenzie_4 means :: ROBBINS5:def 5
 for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1;
end;

:: deftheorem defines satisfying_McKenzie_1 ROBBINS5:def 2 :
for L being non empty LattStr holds
( L is satisfying_McKenzie_1 iff for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 );

:: deftheorem defines satisfying_McKenzie_2 ROBBINS5:def 3 :
for L being non empty LattStr holds
( L is satisfying_McKenzie_2 iff for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 );

:: deftheorem defines satisfying_McKenzie_3 ROBBINS5:def 4 :
for L being non empty LattStr holds
( L is satisfying_McKenzie_3 iff for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 );

:: deftheorem defines satisfying_McKenzie_4 ROBBINS5:def 5 :
for L being non empty LattStr holds
( L is satisfying_McKenzie_4 iff for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 );

theorem MainMcKenzie: :: ROBBINS5:13
for L being non empty LattStr st L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) holds
( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative )
proof end;

theorem AuxiliaryMcKenzie: :: ROBBINS5:14
for L being non empty LattStr st L is join-commutative & L is join-associative & L is meet-commutative & L is meet-associative & ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) holds
( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) )
proof end;

definition
let L be non empty LattStr ;
attr L is satisfying_4_McKenzie_axioms means :: ROBBINS5:def 6
( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 );
end;

:: deftheorem defines satisfying_4_McKenzie_axioms ROBBINS5:def 6 :
for L being non empty LattStr holds
( L is satisfying_4_McKenzie_axioms iff ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 ) );

registration
cluster non empty satisfying_4_McKenzie_axioms -> non empty satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 for LattStr ;
coherence
for b1 being non empty LattStr st b1 is satisfying_4_McKenzie_axioms holds
( b1 is satisfying_McKenzie_1 & b1 is satisfying_McKenzie_2 & b1 is satisfying_McKenzie_3 & b1 is satisfying_McKenzie_4 ) ;
cluster non empty satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 -> non empty satisfying_4_McKenzie_axioms for LattStr ;
coherence
for b1 being non empty LattStr st b1 is satisfying_McKenzie_1 & b1 is satisfying_McKenzie_2 & b1 is satisfying_McKenzie_3 & b1 is satisfying_McKenzie_4 holds
b1 is satisfying_4_McKenzie_axioms ;
end;

theorem CombinedMcKenzie: :: ROBBINS5:15
for L being non empty LattStr holds
( L is Lattice iff L is satisfying_4_McKenzie_axioms )
proof end;

registration
cluster non empty Lattice-like -> non empty satisfying_4_McKenzie_axioms for LattStr ;
coherence
for b1 being non empty LattStr st b1 is Lattice-like holds
b1 is satisfying_4_McKenzie_axioms by CombinedMcKenzie;
cluster non empty satisfying_4_McKenzie_axioms -> non empty Lattice-like for LattStr ;
coherence
for b1 being non empty LattStr st b1 is satisfying_4_McKenzie_axioms holds
b1 is Lattice-like by CombinedMcKenzie;
end;