:: 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 b₁ being non empty LattStr st b₁ is join-absorbing & b₁ is satisfying_Sholander_1 holds
( b₁ is distributive & b₁ is Lattice-like ) by Combined;

cluster non empty join-commutative meet-commutative distributive -> non empty satisfying_Sholander_1 for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is distributive & b₁ is join-commutative & b₁ is meet-commutative holds
b₁ 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 b₁ being non empty LattStr st b₁ is satisfying_4_McKenzie_axioms holds
( b₁ is satisfying_McKenzie_1 & b₁ is satisfying_McKenzie_2 & b₁ is satisfying_McKenzie_3 & b₁ 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 b₁ being non empty LattStr st b₁ is satisfying_McKenzie_1 & b₁ is satisfying_McKenzie_2 & b₁ is satisfying_McKenzie_3 & b₁ is satisfying_McKenzie_4 holds
b₁ 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 b₁ being non empty LattStr st b₁ is Lattice-like holds
b₁ is satisfying_4_McKenzie_axioms by CombinedMcKenzie;

cluster non empty satisfying_4_McKenzie_axioms -> non empty Lattice-like for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is satisfying_4_McKenzie_axioms holds
b₁ is Lattice-like by CombinedMcKenzie;

end;