:: by Adam Grabowski and Damian Sawicki

::

:: Received June 29, 2018

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

definition

let L be non empty LattStr ;

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

for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0);

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

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

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

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

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

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)

for v0, v1, v2 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2)

proof end;

:: Third

theorem :: ROBBINS5:6

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

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)

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)

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)

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;

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

( L is distributive Lattice iff ( L is join-absorbing & L is satisfying_Sholander_1 ) )

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is join-absorbing & b_{1} is satisfying_Sholander_1 holds

( b_{1} is distributive & b_{1} is Lattice-like )
by Combined;

for b_{1} being non empty LattStr st b_{1} is distributive & b_{1} is join-commutative & b_{1} is meet-commutative holds

b_{1} is satisfying_Sholander_1
by LatToSho;

end;

cluster non empty join-absorbing satisfying_Sholander_1 -> non empty Lattice-like distributive for LattStr ;

coherence for b

( b

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

coherence for b

b

definition

let L be non empty LattStr ;

end;
attr L is satisfying_McKenzie_1 means :: ROBBINS5:def 2

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;

attr L is satisfying_McKenzie_2 means :: ROBBINS5:def 3

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;

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;

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;

for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1;

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

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

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

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

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 )

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

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

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

( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 );

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

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

for b_{1} being non empty LattStr st b_{1} is satisfying_4_McKenzie_axioms holds

( b_{1} is satisfying_McKenzie_1 & b_{1} is satisfying_McKenzie_2 & b_{1} is satisfying_McKenzie_3 & b_{1} is satisfying_McKenzie_4 )
;

for b_{1} being non empty LattStr st b_{1} is satisfying_McKenzie_1 & b_{1} is satisfying_McKenzie_2 & b_{1} is satisfying_McKenzie_3 & b_{1} is satisfying_McKenzie_4 holds

b_{1} is satisfying_4_McKenzie_axioms
;

end;

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

( b

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

b

registration

coherence

for b_{1} being non empty LattStr st b_{1} is Lattice-like holds

b_{1} is satisfying_4_McKenzie_axioms
by CombinedMcKenzie;

coherence

for b_{1} being non empty LattStr st b_{1} is satisfying_4_McKenzie_axioms holds

b_{1} is Lattice-like
by CombinedMcKenzie;

end;
for b

b

coherence

for b

b