:: Formalization of Quasilattices
:: by Dominik Kulesza and Adam Grabowski
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

definition

let L be non empty LattStr ;

attr L is satisfying_QLT1 means :: LATQUASI:def 1
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2);

attr L is satisfying_QLT2 means :: LATQUASI:def 2
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2);

attr L is QLT-distributive means :: LATQUASI:def 3
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2);

end;

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

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

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

registration

cluster non empty trivial -> non empty satisfying_QLT1 satisfying_QLT2 QLT-distributive for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is satisfying_QLT1 & b₁ is satisfying_QLT2 & b₁ is QLT-distributive ) by STRUCT_0:def 10;

end;

registration

cluster non empty trivial -> non empty join-idempotent meet-idempotent for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is join-idempotent & b₁ is meet-idempotent )

proof end;

end;

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 for LattStr ;

existence
ex b₁ being non empty LattStr st
( b₁ is join-commutative & b₁ is join-associative & b₁ is join-idempotent & b₁ is meet-commutative & b₁ is meet-associative & b₁ is meet-idempotent & b₁ is satisfying_QLT1 & b₁ is satisfying_QLT2 )

proof end;

end;

definition

let L be non empty join-commutative LattStr ;

redefine attr L is satisfying_QLT1 means :: LATQUASI:def 4
for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2);

compatibility
( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) )

proof end;

end;

:: deftheorem defines satisfying_QLT1 LATQUASI:def 4 :
for L being non empty join-commutative LattStr holds
( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) );

registration

cluster {0,1,2} -> real-membered ;

coherence
{0,1,2} is real-membered ;

end;

registration

cluster -> real for Element of {0,1,2};

coherence
for b₁ being Element of {0,1,2} holds b₁ is real ;

end;

T2: for x, y being Element of {0,1,2} holds min (x,y) in {0,1,2}

proof end;

definition

let x, y be Element of {0,1,2};

func OpEx2 (x,y) -> Element of {0,1,2} equals :OpEx2Def: :: LATQUASI:def 5
1 if ( x = 1 or y = 1 )
min (x,y) if ( x <> 1 & y <> 1 )
;

coherence
( ( ( x = 1 or y = 1 ) implies 1 is Element of {0,1,2} ) & ( x <> 1 & y <> 1 implies min (x,y) is Element of {0,1,2} ) ) by T2;
consistency
for b₁ being Element of {0,1,2} st ( x = 1 or y = 1 ) & x <> 1 & y <> 1 holds
( b₁ = 1 iff b₁ = min (x,y) ) ;

end;

:: deftheorem OpEx2Def defines OpEx2 LATQUASI:def 5 :
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies OpEx2 (x,y) = 1 ) & ( x <> 1 & y <> 1 implies OpEx2 (x,y) = min (x,y) ) );

definition

func QLT_Ex1 -> BinOp of {0,1,2} means :QLTEx1Def: :: LATQUASI:def 6
for x, y being Element of {0,1,2} holds
( ( x = y implies it . (x,y) = x ) & ( x <> y implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds
( ( x = y implies b₁ . (x,y) = x ) & ( x <> y implies b₁ . (x,y) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds
( ( x = y implies b₁ . (x,y) = x ) & ( x <> y implies b₁ . (x,y) = 0 ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( x = y implies b₂ . (x,y) = x ) & ( x <> y implies b₂ . (x,y) = 0 ) ) ) holds
b₁ = b₂

proof end;

func QLT_Ex2 -> BinOp of {0,1,2} means :QLTEx2Def: :: LATQUASI:def 7
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies it . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies it . (x,y) = min (x,y) ) );

existence
ex b₁ being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b₁ . (x,y) = min (x,y) ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b₁ . (x,y) = min (x,y) ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b₂ . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b₂ . (x,y) = min (x,y) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem QLTEx1Def defines QLT_Ex1 LATQUASI:def 6 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = QLT_Ex1 iff for x, y being Element of {0,1,2} holds
( ( x = y implies b₁ . (x,y) = x ) & ( x <> y implies b₁ . (x,y) = 0 ) ) );

:: deftheorem QLTEx2Def defines QLT_Ex2 LATQUASI:def 7 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = QLT_Ex2 iff for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b₁ . (x,y) = min (x,y) ) ) );

theorem WazneQLT7: :: LATQUASI:1

QLT_Ex1 <> QLT_Ex2

proof end;

::: Construction of quasi-lattices needed to prove QLT-7
:: x <= y iff x "\/" y = y
::: if absorption is true, then x <= y iff x "/\" y = x

definition

func QLTLattice1 -> non empty strict LattStr equals :: LATQUASI:def 8
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

coherence
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #) is non empty strict LattStr ;

func QLTLattice2 -> non empty strict LattStr equals :: LATQUASI:def 9
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

coherence
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #) is non empty strict LattStr ;

end;

:: deftheorem defines QLTLattice1 LATQUASI:def 8 :
QLTLattice1 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

:: deftheorem defines QLTLattice2 LATQUASI:def 9 :
QLTLattice2 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

registration

cluster QLT_Ex1 -> commutative associative idempotent ;

coherence
( QLT_Ex1 is commutative & QLT_Ex1 is associative & QLT_Ex1 is idempotent )

proof end;

end;

registration

cluster QLT_Ex2 -> commutative associative idempotent ;

coherence
( QLT_Ex2 is commutative & QLT_Ex2 is associative & QLT_Ex2 is idempotent )

proof end;

end;

registration

cluster QLTLattice1 -> non empty strict join-commutative join-associative join-idempotent ;

coherence
( QLTLattice1 is join-commutative & QLTLattice1 is join-associative & QLTLattice1 is join-idempotent )

proof end;

end;

registration

cluster QLTLattice1 -> non empty strict meet-commutative meet-associative meet-idempotent ;

coherence
( QLTLattice1 is meet-commutative & QLTLattice1 is meet-associative & QLTLattice1 is meet-idempotent )

proof end;

end;

theorem Lemacik00: :: LATQUASI:2

for v0, v1 being Element of QLTLattice1 st v1 = 0 holds
v0 "/\" v1 = v1

proof end;

theorem Lemacik001: :: LATQUASI:3

for v0, v1 being Element of QLTLattice1 st v1 = 0 holds
v0 "\/" v1 = v1

proof end;

registration

cluster QLTLattice1 -> non empty strict satisfying_QLT1 ;

coherence
QLTLattice1 is satisfying_QLT1

proof end;

end;

registration

cluster QLTLattice1 -> non empty strict satisfying_QLT2 ;

coherence
QLTLattice1 is satisfying_QLT2

proof end;

end;

:: Every QLTLattice is QuasiLattice

registration

cluster -> real for Element of the carrier of QLTLattice2;

coherence
for b₁ being Element of QLTLattice2 holds b₁ is real ;

end;

registration

cluster QLTLattice2 -> non empty strict join-commutative join-associative join-idempotent ;

coherence
( QLTLattice2 is join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent )

proof end;

end;

registration

cluster QLTLattice2 -> non empty strict meet-commutative meet-associative meet-idempotent ;

coherence
( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent )

proof end;

end;

registration

cluster QLTLattice2 -> non empty strict satisfying_QLT1 ;

coherence
QLTLattice2 is satisfying_QLT1

proof end;

end;

registration

cluster QLTLattice2 -> non empty strict satisfying_QLT2 ;

coherence
QLTLattice2 is satisfying_QLT2

proof end;

end;

registration

cluster QLTLattice2 -> non empty strict non join-absorbing ;

coherence
not QLTLattice2 is join-absorbing

proof end;

cluster QLTLattice2 -> non empty strict non meet-absorbing ;

coherence
not QLTLattice2 is meet-absorbing

proof end;

end;

registration

cluster QLTLattice1 -> non empty strict non join-absorbing ;

coherence
not QLTLattice1 is join-absorbing

proof end;

cluster QLTLattice1 -> non empty strict non meet-absorbing ;

coherence
not QLTLattice1 is meet-absorbing

proof end;

end;

definition

mode QuasiLattice is non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;

end;

:: In QLT-1 we don't need two QLT axioms:
:: for v0 holds v0"/\"v0 = v0 & :: /\-idempotent
:: (for v2,v1,v0 holds
:: (v0"/\"v1)"/\"v2 = v0"/\"(v1"/\"v2)) & :: /\-associative

theorem Lemma1: :: LATQUASI:4

for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)

proof end;

theorem Cluster1: :: LATQUASI:5

for L being non empty LattStr st L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-distributive holds
L is distributive

proof end;

registration

cluster non empty join-commutative join-associative meet-commutative join-idempotent satisfying_QLT1 satisfying_QLT2 QLT-distributive -> non empty distributive for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-commutative & b₁ is satisfying_QLT1 & b₁ is join-idempotent & b₁ is join-associative & b₁ is join-commutative & b₁ is satisfying_QLT2 & b₁ is QLT-distributive holds
b₁ is distributive by Cluster1;

end;

theorem ThQLT2: :: LATQUASI:6

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

theorem Cluster2: :: LATQUASI:7

for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is join-idempotent & L is join-associative & L is satisfying_QLT2 & L is distributive holds
L is distributive'

proof end;

registration

cluster non empty join-associative meet-commutative meet-associative distributive join-idempotent meet-idempotent satisfying_QLT2 -> non empty distributive' for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-idempotent & b₁ is meet-associative & b₁ is meet-commutative & b₁ is join-idempotent & b₁ is join-associative & b₁ is satisfying_QLT2 & b₁ is distributive holds
b₁ is distributive' by Cluster2;

end;

definition

let L be non empty LattStr ;

attr L is QLT-selfdistributive means :: LATQUASI:def 10
for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0);

end;

:: deftheorem defines QLT-selfdistributive LATQUASI:def 10 :
for L being non empty LattStr holds
( L is QLT-selfdistributive iff for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) );

theorem ThQLT3: :: LATQUASI:8

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

Cluster3: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfdistributive holds
L is distributive'

proof end;

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfdistributive -> non empty distributive' for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-idempotent & b₁ is meet-associative & b₁ is meet-commutative & b₁ is satisfying_QLT1 & b₁ is join-idempotent & b₁ is join-associative & b₁ is join-commutative & b₁ is satisfying_QLT2 & b₁ is QLT-selfdistributive holds
b₁ is distributive' by Cluster3;

end;

definition

let L be non empty LattStr ;

attr L is satisfying_Bowden_inequality means :: LATQUASI:def 11
for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z);

end;

:: deftheorem defines satisfying_Bowden_inequality LATQUASI:def 11 :
for L being non empty LattStr holds
( L is satisfying_Bowden_inequality iff for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z) );

definition

let L be non empty join-commutative LattStr ;

redefine attr L is satisfying_Bowden_inequality means :BowdenRedef: :: LATQUASI:def 12
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2);

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

proof end;

end;

:: deftheorem BowdenRedef defines satisfying_Bowden_inequality LATQUASI:def 12 :
for L being non empty join-commutative LattStr holds
( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) );

theorem ThQLT4: :: LATQUASI:9

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

Cluster4: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is satisfying_Bowden_inequality holds
L is distributive'

proof end;

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 satisfying_Bowden_inequality -> non empty distributive' for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-idempotent & b₁ is meet-associative & b₁ is meet-commutative & b₁ is satisfying_QLT1 & b₁ is join-idempotent & b₁ is join-associative & b₁ is join-commutative & b₁ is satisfying_QLT2 & b₁ is satisfying_Bowden_inequality holds
b₁ is distributive' by Cluster4;

end;

definition

let L be non empty LattStr ;

attr L is QLT-selfmodular means :: LATQUASI:def 13
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1));

end;

:: deftheorem defines QLT-selfmodular LATQUASI:def 13 :
for L being non empty LattStr holds
( L is QLT-selfmodular iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) );

definition

let L be non empty join-idempotent LattStr ;
let a, b be Element of L;
:: original: [=
redefine pred a [= b;
reflexivity
for a being Element of L holds R29(L,b₁,b₁)

proof end;

end;

:: Modularity for Quasilattices

theorem QLTMod: :: LATQUASI:10

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v1, v2 being Element of L st v0 "\/" v1 = v1 holds
v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

ClusterA: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & L is modular holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

theorem QLTMod2: :: LATQUASI:11

for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds
for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2

proof end;

ClusterB: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds
L is modular

proof end;

definition

let L be non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;

redefine attr L is modular means :ModRedef: :: LATQUASI:def 14
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3));

compatibility
( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )

proof end;

end;

:: deftheorem ModRedef defines modular LATQUASI:def 14 :
for L being non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr holds
( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) );

theorem ThQLT5: :: LATQUASI:12

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

Cluster5: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular holds
L is modular

proof end;

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular -> non empty modular for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-idempotent & b₁ is meet-associative & b₁ is meet-commutative & b₁ is satisfying_QLT1 & b₁ is join-idempotent & b₁ is join-associative & b₁ is join-commutative & b₁ is satisfying_QLT2 & b₁ is QLT-selfmodular holds
b₁ is modular by Cluster5;

end;

theorem ThQLT6: :: LATQUASI:13

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

definition

let L be non empty LattStr ;

attr L is QLT-selfmodular' means :: LATQUASI:def 15
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1;

end;

:: deftheorem defines QLT-selfmodular' LATQUASI:def 15 :
for L being non empty LattStr holds
( L is QLT-selfmodular' iff for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 );

Cluster6: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular' holds
L is modular

proof end;

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular' -> non empty modular for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-idempotent & b₁ is meet-associative & b₁ is meet-commutative & b₁ is satisfying_QLT1 & b₁ is join-idempotent & b₁ is join-associative & b₁ is join-commutative & b₁ is satisfying_QLT2 & b₁ is QLT-selfmodular' holds
b₁ is modular by Cluster6;

end;

theorem :: LATQUASI:14

ex L1, L2 being QuasiLattice st
( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )

proof end;