:: Filters - Part II. Quotient Lattices Modulo Filters and
:: Direct Product of Two Lattices
:: by Grzegorz Bancerek
::
:: Received April 19, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICES, CARD_FIL, SUBSET_1, XBOOLE_0, RELAT_1, EQREL_1,
FILTER_0, BINOP_1, PBOOLE, FUNCT_1, MCART_1, TARSKI, LATTICE2, STRUCT_0,
XBOOLEAN, FUNCT_4, ZFMISC_1, WELLORD1, XXREAL_2, PARTFUN1, FILTER_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, EQREL_1, DOMAIN_1, WELLORD1, FUNCT_3, FUNCT_4,
STRUCT_0, LATTICES, FILTER_0, LATTICE2;
constructors WELLORD1, BINOP_1, FUNCT_3, FUNCT_4, EQREL_1, REALSET1, FILTER_0,
LATTICE2, RELSET_1;
registrations SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, EQREL_1, STRUCT_0,
LATTICES, FILTER_0, LATTICE2, RELSET_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, WELLORD1, BINOP_1, FILTER_0, LATTICE2, LATTICES,
XBOOLE_0;
equalities BINOP_1, FILTER_0, LATTICE2, LATTICES, XBOOLE_0;
expansions BINOP_1, LATTICES;
theorems FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, WELLORD1, DOMAIN_1, EQREL_1,
RELAT_1, ZFMISC_1, LATTICES, FILTER_0, LATTICE2, RELSET_1, XBOOLE_0,
XBOOLE_1, SUBSET_1, XTUPLE_0, TARSKI;
schemes FUNCT_1, FUNCT_2, BINOP_1;
begin
deffunc join(LattStr) = the L_join of $1;
deffunc meet(LattStr) = the L_meet of $1;
reserve L,L1,L2 for Lattice,
F1,F2 for Filter of L,
p,q,r,s for Element of L,
p1,q1,r1,s1 for Element of L1,
p2,q2,r2,s2 for Element of L2,
X,x,x1,x2,y,y1,y2 for set,
D,D1,D2 for non empty set,
R for Relation,
RD for Equivalence_Relation of D,
a,b,d for Element of D,
a1,b1,c1 for Element of D1,
a2,b2,c2 for Element of D2,
B for B_Lattice,
FB for Filter of B,
I for I_Lattice,
FI for Filter of I ,
i,i1,i2,j,j1,j2,k for Element of I,
f1,g1 for BinOp of D1,
f2,g2 for BinOp of D2;
theorem Th1:
F1 /\ F2 is Filter of L
proof
consider p such that
A1: p in F1 by SUBSET_1:4;
consider q such that
A2: q in F2 by SUBSET_1:4;
A3: p "\/" q in F2 by A2,FILTER_0:10;
p "\/" q in F1 by A1,FILTER_0:10;
then reconsider D = F1 /\ F2 as non empty Subset of L by A3,XBOOLE_0:def 4;
now
let p,q;
p "/\" q in F1 & p "/\" q in F2 iff p in F1 & q in F1 & p in F2 & q in
F2 by FILTER_0:8;
hence p in F1 /\ F2 & q in F1 /\ F2 iff
p "/\" q in F1 /\ F2 by XBOOLE_0:def 4;
end;
then D is Filter of L by FILTER_0:8;
hence thesis;
end;
theorem
<.p.) = <.q.) implies p = q
proof
assume
A1: <.p.) = <.q.);
then q in <.p.);
then
A2: p [= q by FILTER_0:15;
p in <.q.) by A1;
then q [= p by FILTER_0:15;
hence thesis by A2,LATTICES:8;
end;
definition
let L,F1,F2;
redefine func F1 /\ F2 -> Filter of L; :: redefines /\ (XBOOLE_0, definition)
coherence by Th1;
end;
definition
let D,R;
mode UnOp of D,R -> UnOp of D means
:Def1:
for x,y being Element of D st [x, y] in R holds [it.x,it.y] in R;
existence
proof
reconsider f = id D as UnOp of D;
take f;
let x,y be Element of D;
thus thesis;
end;
mode BinOp of D,R -> BinOp of D means
:Def2:
for x1,y1, x2,y2 being Element
of D st [x1,y1] in R & [x2,y2] in R holds [it.(x1,x2),it.(y1,y2)] in R;
existence
proof
take f = pr1(D,D);
let x1,y1, x2,y2 be Element of D;
f.(x1,x2) = x1 by FUNCT_3:def 4;
hence thesis by FUNCT_3:def 4;
end;
end;
reserve F,G for BinOp of D,RD;
definition
let D;
let R be Equivalence_Relation of D;
mode UnOp of R is UnOp of D,R;
mode BinOp of R is BinOp of D,R;
end;
definition
let D;
let R be Equivalence_Relation of D;
let u be UnOp of D;
assume
A1: u is UnOp of D,R;
func u /\/ R -> UnOp of Class R means
for x,y st x in Class R & y in x holds it.x = Class(R,u.y);
existence
proof
now
let X;
assume X in Class R;
then ex x being object st x in D & X = Class(R,x) by EQREL_1:def 3;
hence X <> {} by EQREL_1:20;
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X st X in Class R holds g.X in X by FUNCT_1:111;
A4: rng g c= D
proof
let x be object;
assume x in rng g;
then consider y being object such that
A5: y in dom g and
A6: x = g.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
x in y by A2,A3,A5,A6;
hence thesis by A2,A5;
end;
deffunc F(Element of D) = EqClass(R,$1);
consider f being Function of D, Class R such that
A7: for x being Element of D holds f.x = F(x) from FUNCT_2:sch 4;
reconsider g as Function of Class R, D by A2,A4,FUNCT_2:def 1,RELSET_1:4;
take uR = f*u*g;
let x,y;
assume that
A8: x in Class R and
A9: y in x;
A10: D = dom (f*u) by FUNCT_2:def 1;
g.x in rng g by A2,A8,FUNCT_1:def 3;
then
A11: (f*u).(g.x) = f.(u.(g.x)) by A4,A10,FUNCT_1:12;
Class R = dom uR by FUNCT_2:def 1;
then
A12: uR.x = (f*u).(g.x) by A8,FUNCT_1:12;
reconsider x9 = x as Element of Class R by A8;
reconsider y9 = y as Element of D by A8,A9;
A13: ex x1 being object st x1 in D & x9 = Class(R,x1) by EQREL_1:def 3;
g.x9 in x by A3;
then [g.x9,y9] in R by A9,A13,EQREL_1:22;
then [u.(g.x9),u.y9] in R by A1,Def1;
then
A14: u.(g.x9) in EqClass(R,u.y9) by EQREL_1:19;
f.(u.(g.x9)) = EqClass(R,u.(g.x9)) by A7;
hence thesis by A12,A11,A14,EQREL_1:23;
end;
uniqueness
proof
let u1,u2 be UnOp of Class R such that
A15: for x,y st x in Class R & y in x holds u1.x = Class(R,u.y) and
A16: for x,y st x in Class R & y in x holds u2.x = Class(R,u.y);
now
let x be object;
assume
A17: x in Class R;
then consider y being object such that
A18: y in D and
A19: x = Class(R,y) by EQREL_1:def 3;
u1.x = Class(R,u.y) by A15,A17,A18,A19,EQREL_1:20;
hence u1.x = u2.x by A16,A17,A18,A19,EQREL_1:20;
end;
hence thesis by FUNCT_2:12;
end;
end;
definition
let D;
let R be Equivalence_Relation of D;
let b be BinOp of D;
assume
A1: b is BinOp of D,R;
func b /\/ R -> BinOp of Class R means
:Def4:
for x,y, x1,y1 st x in Class R
& y in Class R & x1 in x & y1 in y holds it.(x,y) = Class(R,b.(x1,y1));
existence
proof
now
let X;
assume X in Class R;
then ex x being object st x in D & X = Class(R,x) by EQREL_1:def 3;
hence X <> {} by EQREL_1:20;
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X st X in Class R holds g.X in X by FUNCT_1:111;
A4: rng g c= D
proof
let x be object;
assume x in rng g;
then consider y being object such that
A5: y in dom g and
A6: x = g.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
x in y by A2,A3,A5,A6;
hence thesis by A2,A5;
end;
deffunc F(Element of D) = EqClass(R,$1);
consider f being Function of D, Class R such that
A7: for x being Element of D holds f.x = F(x) from FUNCT_2:sch 4;
reconsider g as Function of Class R, D by A2,A4,FUNCT_2:def 1,RELSET_1:4;
deffunc F(Element of Class R,Element of Class R) = f.(b.(g.$1,g.$2));
consider bR being BinOp of Class R such that
A8: for x,y being Element of Class R holds bR.(x,y) = F(x,y) from
BINOP_1:sch 4;
take bR;
let x,y, x1,y1;
assume that
A9: x in Class R and
A10: y in Class R and
A11: x1 in x and
A12: y1 in y;
reconsider x9 = x, y9 = y as Element of Class R by A9,A10;
reconsider x19 = x1, y19 = y1 as Element of D by A9,A10,A11,A12;
A13: ex y2 being object st y2 in D & y9 = Class(R,y2) by EQREL_1:def 3;
g.y9 in y by A3;
then
A14: [g.y9,y19] in R by A12,A13,EQREL_1:22;
A15: ex x2 being object st x2 in D & x9 = Class(R,x2) by EQREL_1:def 3;
g.x9 in x by A3;
then [g.x9,x19] in R by A11,A15,EQREL_1:22;
then [b.(g.x9,g.y9),b.(x19,y19)] in R by A1,A14,Def2;
then
A16: b.(g.x9,g.y9) in EqClass(R,b.(x19,y19)) by EQREL_1:19;
A17: f.(b.(g.x9,g.y9)) = EqClass(R,b.(g.x9,g.y9)) by A7;
bR.(x9,y9) = f.(b.(g.x9,g.y9)) by A8;
hence thesis by A16,A17,EQREL_1:23;
end;
uniqueness
proof
let b1,b2 be BinOp of Class R such that
A18: for x,y, x1,y1 st x in Class R & y in Class R & x1 in x & y1 in y
holds b1.(x,y) = Class(R,b.(x1,y1)) and
A19: for x,y, x1,y1 st x in Class R & y in Class R & x1 in x & y1 in y
holds b2.(x,y) = Class(R,b.(x1,y1));
now
let x,y be Element of Class R;
consider x1 being object such that
A20: x1 in D and
A21: x = Class(R,x1) by EQREL_1:def 3;
consider y1 being object such that
A22: y1 in D and
A23: y = Class(R,y1) by EQREL_1:def 3;
A24: y1 in y by A22,A23,EQREL_1:20;
A25: x1 in x by A20,A21,EQREL_1:20;
then b1.(x,y) = Class(R,b.(x1,y1)) by A18,A24;
hence b1.(x,y) = b2.(x,y) by A19,A25,A24;
end;
hence thesis;
end;
end;
theorem Th3:
(F /\/ RD).(Class(RD,a), Class(RD,b)) = Class(RD, F.(a,b))
proof
A1: b in EqClass(RD,b) by EQREL_1:20;
a in EqClass(RD,a) by EQREL_1:20;
hence thesis by A1,Def4;
end;
scheme
SchAux1 { D()->non empty set, R()->Equivalence_Relation of D(), P[set] }:
for x being Element of Class R() holds P[x]
provided
A1: for x being Element of D() holds P[EqClass(R(),x)]
proof
let x be Element of Class R();
ex y being object st y in D() & x = Class(R(),y) by EQREL_1:def 3;
hence thesis by A1;
end;
scheme
SchAux2 { D()->non empty set, R()->Equivalence_Relation of D(), P[set,set] }
: for x,y being Element of Class R() holds P[x,y]
provided
A1: for x,y being Element of D() holds P[EqClass(R(),x),EqClass(R(),y)]
proof
let x1,x2 be Element of Class R();
A2: ex y2 being object st y2 in D() & x2 = Class(R(),y2) by EQREL_1:def 3;
ex y1 being object st y1 in D() & x1 = Class(R(),y1) by EQREL_1:def 3;
hence thesis by A1,A2;
end;
scheme
SchAux3 { D()->non empty set, R()->Equivalence_Relation of D(), P[set,set,
set] }: for x,y,z being Element of Class R() holds P[x,y,z]
provided
A1: for x,y,z being Element of D() holds P[EqClass(R(),x),EqClass(R(),y)
,EqClass(R(),z)]
proof
let x1,x2,x3 be Element of Class R();
A2: ex y2 being object st y2 in D() & x2 = Class(R(),y2) by EQREL_1:def 3;
A3: ex y3 being object st y3 in D() & x3 = Class(R(),y3) by EQREL_1:def 3;
ex y1 being object st y1 in D() & x1 = Class(R(),y1) by EQREL_1:def 3;
hence thesis by A1,A2,A3;
end;
theorem Th4:
F is commutative implies F/\/RD is commutative
proof
defpred P[Element of Class RD, Element of Class RD] means (F/\/RD).($1,$2) =
(F/\/RD).($2,$1);
assume
A1: for a,b holds F.(a,b) = F.(b,a);
A2: now
let x1,x2 be Element of D;
(F/\/RD).(EqClass(RD,x1),EqClass(RD,x2)) = Class(RD, F.(x1,x2)) by Th3
.= Class(RD, F.(x2,x1)) by A1
.= (F/\/RD).(EqClass(RD,x2),EqClass(RD,x1)) by Th3;
hence P[EqClass(RD,x1),EqClass(RD,x2)];
end;
thus for c1,c2 being Element of Class RD holds P[c1,c2] from SchAux2( A2);
end;
theorem Th5:
F is associative implies F/\/RD is associative
proof
defpred P[Element of Class RD, Element of Class RD, Element of Class RD]
means (F/\/RD).($1,(F/\/RD).($2,$3)) = (F/\/RD).((F/\/RD).($1,$2),$3);
assume
A1: for d,a,b holds F.(d,F.(a,b)) = F.(F.(d,a),b);
A2: now
let x1,x2,x3 be Element of D;
(F/\/RD).(EqClass(RD,x1), (F/\/RD).(EqClass(RD,x2),EqClass(RD,x3))) =
(F/\/RD).(Class(RD,x1),Class(RD, F.(x2,x3))) by Th3
.= Class(RD, F.(x1,F.(x2,x3))) by Th3
.= Class(RD, F.(F.(x1,x2),x3)) by A1
.= (F/\/RD).(Class(RD,F.(x1,x2)),Class(RD, x3)) by Th3
.= (F/\/RD).((F/\/RD).(EqClass(RD,x1),EqClass(RD,x2)), EqClass(RD,x3))
by Th3;
hence P[EqClass(RD,x1),EqClass(RD,x2),EqClass(RD,x3)];
end;
thus for c1,c2,c3 being Element of Class RD holds P[c1,c2,c3] from SchAux3(
A2);
end;
theorem Th6:
d is_a_left_unity_wrt F implies EqClass(RD,d) is_a_left_unity_wrt F/\/RD
proof
defpred P[Element of Class RD] means (F/\/RD).(EqClass(RD,d),$1) = $1;
assume
A1: F.(d,a) = a;
A2: now
let a;
(F/\/RD).(EqClass(RD,d),EqClass(RD,a)) = Class(RD, F.(d,a)) by Th3
.= EqClass(RD, a) by A1;
hence P[EqClass(RD,a)];
end;
thus for c being Element of Class RD holds P[c] from SchAux1(A2);
end;
theorem Th7:
d is_a_right_unity_wrt F implies EqClass(RD,d) is_a_right_unity_wrt F/\/RD
proof
defpred P[Element of Class RD] means (F/\/RD).($1,EqClass(RD,d)) = $1;
assume
A1: F.(a,d) = a;
A2: now
let a;
(F/\/RD).(EqClass(RD,a),EqClass(RD,d)) = EqClass(RD, F.(a,d)) by Th3
.= EqClass(RD, a) by A1;
hence P[EqClass(RD,a)];
end;
thus for c being Element of Class RD holds P[c] from SchAux1(A2);
end;
theorem
d is_a_unity_wrt F implies EqClass(RD,d) is_a_unity_wrt F/\/RD
by Th6,Th7;
theorem Th9:
F is_left_distributive_wrt G implies F/\/RD is_left_distributive_wrt G/\/RD
proof
deffunc Cl(Element of D) = EqClass(RD,$1);
defpred P[Element of Class RD, Element of Class RD, Element of Class RD]
means (F/\/RD).($1,(G/\/RD).($2,$3)) = (G/\/RD).((F/\/RD).($1,$2),(F/\/RD).($1,
$3));
assume
A1: for d,a,b holds F.(d,G.(a,b)) = G.(F.(d,a),F.(d,b));
A2: now
let x1,x2,x3 be Element of D;
(F/\/RD).(Cl(x1),(G/\/RD).(Cl(x2),Cl(x3))) = (F/\/RD).(Cl(x1),Cl(G.(x2
,x3))) by Th3
.= Cl(F.(x1,G.(x2,x3))) by Th3
.= Cl(G.(F.(x1,x2),F.(x1,x3))) by A1
.= (G/\/RD).(Cl(F.(x1,x2)),Cl(F.(x1,x3))) by Th3
.= (G/\/RD).((F/\/RD).(Cl(x1),Cl(x2)),Cl(F.(x1,x3))) by Th3
.= (G/\/RD).((F/\/RD).(Cl(x1),Cl(x2)),(F/\/RD).(Cl(x1),Cl(x3))) by Th3;
hence P[EqClass(RD,x1),EqClass(RD,x2),EqClass(RD,x3)];
end;
thus for c1,c2,c3 being Element of Class RD holds P[c1,c2,c3] from SchAux3(
A2);
end;
theorem Th10:
F is_right_distributive_wrt G implies F/\/RD is_right_distributive_wrt G/\/RD
proof
deffunc Cl(Element of D) = EqClass(RD,$1);
defpred P[Element of Class RD, Element of Class RD, Element of Class RD]
means (F/\/RD).((G/\/RD).($1,$2),$3) = (G/\/RD).((F/\/RD).($1,$3),(F/\/RD).($2,
$3));
assume
A1: for a,b,d holds F.(G.(a,b),d) = G.(F.(a,d),F.(b,d));
A2: now
let x2,x3,x1 be Element of D;
(F/\/RD).((G/\/RD).(Cl(x2),Cl(x3)),Cl(x1)) = (F/\/RD).(Cl(G.(x2,x3)),
Cl(x1)) by Th3
.= Cl(F.(G.(x2,x3),x1)) by Th3
.= Cl(G.(F.(x2,x1),F.(x3,x1))) by A1
.= (G/\/RD).(Cl(F.(x2,x1)),Cl(F.(x3,x1))) by Th3
.= (G/\/RD).((F/\/RD).(Cl(x2),Cl(x1)),Cl(F.(x3,x1))) by Th3
.= (G/\/RD).((F/\/RD).(Cl(x2),Cl(x1)),(F/\/RD).(Cl(x3),Cl(x1))) by Th3;
hence P[EqClass(RD,x2),EqClass(RD,x3),EqClass(RD,x1)];
end;
thus for c2,c3,c1 being Element of Class RD holds P[c2,c3,c1] from SchAux3(
A2);
end;
theorem
F is_distributive_wrt G implies F/\/RD is_distributive_wrt G/\/RD
by Th9,Th10;
theorem Th12:
F absorbs G implies F/\/RD absorbs G/\/RD
proof
deffunc Cl(Element of D) = EqClass(RD,$1);
defpred P[Element of Class RD,Element of Class RD] means (F/\/RD).($1,(G/\/
RD).($1,$2)) = $1;
assume
A1: for x,y being Element of D holds F.(x,G.(x,y)) = x;
A2: now
let x1,x2 be Element of D;
(F/\/RD).(Cl(x1),(G/\/RD).(Cl(x1),Cl(x2))) = (F/\/RD).(Cl(x1),Cl(G.(x1
,x2))) by Th3
.= Cl(F.(x1,G.(x1,x2))) by Th3
.= Cl(x1) by A1;
hence P[EqClass(RD,x1),EqClass(RD,x2)];
end;
thus for x,y being Element of Class RD holds P[x,y] from SchAux2(A2);
end;
theorem Th13:
the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
proof
set R = equivalence_wrt FI;
let x1,y1, x2,y2 be Element of (the carrier of I);
assume that
A1: [x1,y1] in R and
A2: [x2,y2] in R;
A3: x2 <=> y2 in FI by A2,FILTER_0:def 11;
then
A4: x2 => y2 in FI by FILTER_0:8;
A5: x1 "/\" (x1 => y1) [= y1 by FILTER_0:def 7;
x1 "/\" ((x1 => y1) "/\" (x2 => y2)) = x1 "/\" (x1 => y1) "/\" (x2 =>
y2 ) by LATTICES:def 7;
then
A6: x1 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 by A5,FILTER_0:2;
A7: x2 "/\" ((x1 => y1) "/\" (x2 => y2)) = x2 "/\" (x1 => y1) "/\" (x2 =>
y2 ) by LATTICES:def 7;
A8: x2 "/\" (x2 => y2) [= y2 by FILTER_0:def 7;
(x1 => y1) "/\" (x2 "/\" (x2 => y2)) = (x1 => y1) "/\" x2 "/\" (x2 => y2
) by LATTICES:def 7;
then x2 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y2 by A7,A8,FILTER_0:2;
then
x1 "/\" ((x1 => y1) "/\" (x2 => y2)) "\/" (x2 "/\" ((x1 => y1) "/\" (x2
=> y2))) [= y1 "\/" y2 by A6,FILTER_0:4;
then (x1 "\/" x2) "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 "\/" y2 by
LATTICES:def 11;
then
A9: (x1 => y1) "/\" (x2 => y2) [= (x1 "\/" x2) => (y1 "\/" y2) by
FILTER_0:def 7;
A10: y1 "/\" (y1 => x1) [= x1 by FILTER_0:def 7;
y1 "/\" ((y1 => x1) "/\" (y2 => x2)) = y1 "/\" (y1 => x1) "/\" (y2 =>
x2) by LATTICES:def 7;
then
A11: y1 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 by A10,FILTER_0:2;
A12: y2 "/\" ((y1 => x1) "/\" (y2 => x2)) = y2 "/\" (y1 => x1) "/\" (y2 =>
x2) by LATTICES:def 7;
A13: y2 => x2 in FI by A3,FILTER_0:8;
A14: y2 "/\" (y2 => x2) [= x2 by FILTER_0:def 7;
(y1 => x1) "/\" (y2 "/\" (y2 => x2)) = (y1 => x1) "/\" y2 "/\" (y2 =>
x2) by LATTICES:def 7;
then y2 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x2 by A12,A14,FILTER_0:2;
then
y1 "/\" ((y1 => x1) "/\" (y2 => x2)) "\/" (y2 "/\" ((y1 => x1) "/\" (y2
=> x2))) [= x1 "\/" x2 by A11,FILTER_0:4;
then (y1 "\/" y2) "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 "\/" x2 by
LATTICES:def 11;
then
A15: (y1 => x1) "/\" (y2 => x2) [= (y1 "\/" y2) => (x1 "\/" x2) by
FILTER_0:def 7;
A16: x1 <=> y1 in FI by A1,FILTER_0:def 11;
then y1 => x1 in FI by FILTER_0:8;
then (y1 => x1) "/\" (y2 => x2) in FI by A13,FILTER_0:8;
then
A17: (y1 "\/" y2) => (x1 "\/" x2) in FI by A15,FILTER_0:9;
x1 => y1 in FI by A16,FILTER_0:8;
then (x1 => y1) "/\" (x2 => y2) in FI by A4,FILTER_0:8;
then (x1 "\/" x2) => (y1 "\/" y2) in FI by A9,FILTER_0:9;
then (x1 "\/" x2) <=> (y1 "\/" y2) in FI by A17,FILTER_0:8;
hence thesis by FILTER_0:def 11;
end;
theorem Th14:
the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI
proof
set R = equivalence_wrt FI;
let x1,y1, x2,y2 be Element of I;
assume that
A1: [x1,y1] in R and
A2: [x2,y2] in R;
A3: x2 <=> y2 in FI by A2,FILTER_0:def 11;
then
A4: x2 => y2 in FI by FILTER_0:8;
A5: x1 <=> y1 in FI by A1,FILTER_0:def 11;
then x1 => y1 in FI by FILTER_0:8;
then
A6: (x1 => y1) "/\" (x2 => y2) in FI by A4,FILTER_0:8;
A7: y2 "/\" (y2 => x2) [= x2 by FILTER_0:def 7;
y1 "/\" (y1 => x1) [= x1 by FILTER_0:def 7;
then
A8: y1 "/\" (y1 => x1) "/\" (y2 "/\" (y2 => x2)) [= x1 "/\" x2 by A7,FILTER_0:5
;
A9: x1 "/\" x2 "/\" (x1 => y1) "/\" (x2 => y2) = x1 "/\" x2 "/\" ((x1 => y1
) "/\" (x2 => y2)) by LATTICES:def 7;
A10: x2 "/\" (x2 => y2) [= y2 by FILTER_0:def 7;
x1 "/\" (x1 => y1) [= y1 by FILTER_0:def 7;
then
A11: x1 "/\" (x1 => y1) "/\" (x2 "/\" (x2 => y2)) [= y1 "/\" y2 by A10,
FILTER_0:5;
A12: x2 "/\" x1 "/\" (x1 => y1) = x2 "/\" (x1 "/\" (x1 => y1)) by
LATTICES:def 7;
A13: y2 => x2 in FI by A3,FILTER_0:8;
A14: y2 "/\" y1 "/\" (y1 => x1) = y2 "/\" (y1 "/\" (y1 => x1)) by
LATTICES:def 7;
y1 => x1 in FI by A5,FILTER_0:8;
then
A15: (y1 => x1) "/\" (y2 => x2) in FI by A13,FILTER_0:8;
A16: y1 "/\" y2 "/\" (y1 => x1) "/\" (y2 => x2) = y1 "/\" y2 "/\" ((y1 => x1
) "/\" (y2 => x2)) by LATTICES:def 7;
y1 "/\" (y1 => x1) "/\" (y2 "/\" (y2 => x2)) = y1 "/\" (y1 => x1) "/\"
y2 "/\" (y2 => x2) by LATTICES:def 7;
then (y1 => x1) "/\" (y2 => x2) [= (y1 "/\" y2) => (x1 "/\" x2) by A14,A16,A8
,FILTER_0:def 7;
then
A17: (y1 "/\" y2) => (x1 "/\" x2) in FI by A15,FILTER_0:9;
x1 "/\" (x1 => y1) "/\" (x2 "/\" (x2 => y2)) = x1 "/\" (x1 => y1) "/\"
x2 "/\" (x2 => y2) by LATTICES:def 7;
then (x1 => y1) "/\" (x2 => y2) [= (x1 "/\" x2) => (y1 "/\" y2) by A12,A9,A11
,FILTER_0:def 7;
then (x1 "/\" x2) => (y1 "/\" y2) in FI by A6,FILTER_0:9;
then (x1 "/\" x2) <=> (y1 "/\" y2) in FI by A17,FILTER_0:8;
hence thesis by FILTER_0:def 11;
end;
definition
let L be Lattice, F be Filter of L;
assume
A1: L is I_Lattice;
func L /\/ F -> strict Lattice means
: Def5:
for R being
Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds it =
LattStr (#Class R, (the L_join of L)/\/R, (the L_meet of L)/\/R#);
existence
proof
reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I;
reconsider j = the L_join of I, m = the L_meet of I as BinOp of
equivalence_wrt FI by Th13,Th14;
reconsider LL = LattStr (#Class equivalence_wrt FI, j/\/equivalence_wrt FI
, m/\/equivalence_wrt FI#) as non empty strict LattStr;
A2: join(LL) is commutative by Th4;
A3: join(LL) is associative by Th5;
A4: meet(LL) is associative by Th5;
A5: meet(LL) is commutative by Th4;
A6: meet(LL) absorbs join(LL) by Th12,LATTICE2:27;
join(LL) absorbs meet(LL) by Th12,LATTICE2:26;
then reconsider LL as strict Lattice by A2,A3,A5,A4,A6,LATTICE2:11;
take LL;
thus thesis;
end;
uniqueness
proof
reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I;
set R = equivalence_wrt FI;
reconsider o1 = join(L), o2 = meet(L) as BinOp of R by Th13,Th14;
let L1, L2 be strict Lattice such that
A7: for R being Equivalence_Relation of the carrier of L st R =
equivalence_wrt F holds L1 = LattStr (#Class R, (the L_join of L)/\/R, (the
L_meet of L)/\/R#) and
A8: for R being Equivalence_Relation of the carrier of L st R =
equivalence_wrt F holds L2 = LattStr (#Class R, (the L_join of L)/\/R, (the
L_meet of L)/\/R#);
thus L1 = LattStr (#Class R, o1/\/R, o2/\/R#) by A7
.= L2 by A8;
end;
end;
definition
let L be Lattice, F be Filter of L, a be Element of L;
assume
A1: L is I_Lattice;
func a /\/ F -> Element of L /\/ F means
:Def6:
for R being
Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds it =
Class(R, a);
existence
proof
reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I;
set R = equivalence_wrt FI;
reconsider j = join(I), m = meet(I) as BinOp of R by Th13,Th14;
reconsider i = a as Element of I;
I /\/ FI = LattStr (#Class R, j/\/R, m/\/R#) by Def5;
then reconsider c = EqClass(equivalence_wrt FI,i) as Element of L/\/F;
take c;
thus thesis;
end;
uniqueness
proof
reconsider I = L as I_Lattice by A1;
let c1,c2 be Element of L /\/ F such that
A2: for R being Equivalence_Relation of the carrier of L st R =
equivalence_wrt F holds c1 = Class(R, a) and
A3: for R being Equivalence_Relation of the carrier of L st R =
equivalence_wrt F holds c2 = Class(R, a);
reconsider FI = F as Filter of I;
c1 = Class(equivalence_wrt FI, a) by A2;
hence thesis by A3;
end;
end;
theorem Th15:
(i/\/FI) "\/" (j/\/FI) = (i"\/"j)/\/FI & (i/\/FI) "/\" (j/\/FI)
= (i"/\"j)/\/FI
proof
set R = equivalence_wrt FI;
A1: j/\/FI = Class(R,j) by Def6;
reconsider jj = join(I), mm = meet(I) as BinOp of R by Th13,Th14;
A2: i/\/FI = Class(R,i) by Def6;
A3: I /\/ FI = LattStr (#Class R, jj/\/R, mm/\/R#) by Def5;
(i"\/"j)/\/FI = Class(R,i"\/"j) by Def6;
hence (i/\/FI) "\/" (j/\/FI) = (i"\/"j)/\/FI by A2,A1,A3,Th3;
(i"/\"j)/\/FI = Class(R,i"/\"j) by Def6;
hence thesis by A2,A1,A3,Th3;
end;
theorem Th16:
i/\/FI [= j/\/FI iff i => j in FI
proof
set R = equivalence_wrt FI;
set a = i"\/"j;
set b = a => j;
A1: j"/\"(i => j) [= j by FILTER_0:2;
A2: j"\/"j = j;
thus i/\/FI [= j/\/FI implies i => j in FI
proof
assume (i/\/FI) "\/" (j/\/FI) = j/\/FI;
then
A3: (i"\/"j)/\/FI = j/\/FI by Th15;
A4: i"\/"j in Class(R,i"\/"j) by EQREL_1:20;
A5: i"/\"b [= (i"/\"b)"\/"(j"/\"b) by LATTICES:5;
A6: j/\/FI = Class(R,j) by Def6;
A7: j in Class(R,j) by EQREL_1:20;
Class(R,i"\/"j) = (i"\/"j)/\/FI by Def6;
then [i"\/"j,j] in R by A3,A6,A4,A7,EQREL_1:22;
then (i"\/"j) <=> j in FI by FILTER_0:def 11;
then
A8: (i"\/"j) => j in FI by FILTER_0:8;
A9: a"/\"b [= j by FILTER_0:def 7;
a"/\"b = (i"/\"b)"\/"(j"/\"b) by LATTICES:def 11;
then i"/\"b [= j by A9,A5,LATTICES:7;
then (i"\/"j) => j [= i => j by FILTER_0:def 7;
hence thesis by A8,FILTER_0:9;
end;
j [= i"\/"j by FILTER_0:3;
then j"/\"Top I [= i"\/"j;
then
A10: Top I [= j => (i"\/"j) by FILTER_0:def 7;
Top I in FI by FILTER_0:11;
then
A11: j => (i"\/"j) in FI by A10;
A12: (i"/\"(i => j))"\/"(j"/\"(i => j)) = (i"\/"j)"/\"(i => j) by
LATTICES:def 11;
i"/\"(i => j) [= j by FILTER_0:def 7;
then (i"\/"j)"/\"(i => j) [= j by A1,A2,A12,FILTER_0:4;
then
A13: i => j [= (i"\/"j) => j by FILTER_0:def 7;
assume i => j in FI;
then (i"\/"j) => j in FI by A13,FILTER_0:9;
then (i"\/"j) <=> j in FI by A11,FILTER_0:8;
then
A14: [i"\/"j,j] in R by FILTER_0:def 11;
thus (i/\/FI) "\/" (j/\/FI) = (i"\/"j)/\/FI by Th15
.= Class(R,i"\/"j) by Def6
.= Class(R,j) by A14,EQREL_1:35
.= j/\/FI by Def6;
end;
theorem Th17:
(i"/\"j) => k = i => (j => k)
proof
A1: (j"/\"i)"/\"((i"/\"j)=>k) = j"/\"(i "/\" ( ( i "/\"j)=>k)) by
LATTICES:def 7;
(i"/\"j)"/\"((i"/\"j)=>k) [= k by FILTER_0:def 7;
then i"/\"((i"/\"j)=>k) [= j=>k by A1,FILTER_0:def 7;
then
A2: (i"/\"j)=>k [= i=>(j=>k) by FILTER_0:def 7;
A3: j"/\"(i"/\"(i=>(j=>k))) = j"/\"i"/\"(i=>(j=>k)) by LATTICES:def 7;
i"/\"(i=>(j=>k)) [= j=>k by FILTER_0:def 7;
then
A4: j"/\"(i"/\"(i=>(j=>k))) [= j"/\"(j=>k) by LATTICES:9;
j"/\"(j=>k) [= k by FILTER_0:def 7;
then i"/\"j"/\"(i=>(j=>k)) [= k by A4,A3,LATTICES:7;
then i=>(j=>k) [= (i"/\"j)=>k by FILTER_0:def 7;
hence thesis by A2,LATTICES:8;
end;
theorem Th18:
I is lower-bounded implies I/\/FI is 0_Lattice & Bottom (I/\/FI)
= (Bottom I)/\/FI
proof
set L = I/\/FI;
set R = equivalence_wrt FI;
assume
A1: I is lower-bounded;
then consider i such that
A2: i"/\"j = i & j"/\"i = i;
set x = i/\/FI;
A3: now
let y be Element of L;
L = LattStr (#Class R, (the L_join of I)/\/R, (the L_meet of I)/\/R #)
by Def5;
then consider j such that
A4: y = Class(R,j) by EQREL_1:36;
A5: i"/\"j = i by A2;
A6: y = j/\/FI by A4,Def6;
hence x"/\"y = x by A5,Th15;
thus y"/\"x = x by A5,A6,Th15;
end;
hence
A7: I/\/FI is 0_Lattice by LATTICES:def 13;
Bottom I = i by A1,A2,LATTICES:def 16;
hence thesis by A3,A7,LATTICES:def 16;
end;
theorem Th19:
I/\/FI is 1_Lattice & Top (I/\/FI) = (Top I)/\/FI
proof
set L = I/\/FI;
set R = equivalence_wrt FI;
set x = (Top I)/\/FI;
A1: now
let y be Element of L;
L = LattStr (#Class R, (the L_join of I)/\/R, (the L_meet of I)/\/R #)
by Def5;
then consider j such that
A2: y = Class(R,j) by EQREL_1:36;
A3: (Top I)"\/"j = Top I;
A4: y = j/\/FI by A2,Def6;
hence x"\/"y = x by A3,Th15;
thus y"\/"x = x by A3,A4,Th15;
end;
hence I/\/FI is 1_Lattice by LATTICES:def 14;
hence thesis by A1,LATTICES:def 17;
end;
registration
let I,FI;
cluster I/\/FI -> implicative;
coherence
proof
set L = I/\/FI;
set R = equivalence_wrt FI;
let x,y be Element of L;
A1: Top I in FI by FILTER_0:11;
A2: L = LattStr (#Class R, (the L_join of I)/\/R, (the L_meet of I)/\/R#) by
Def5;
then consider i such that
A3: x = Class(R,i) by EQREL_1:36;
A4: x = i/\/FI by A3,Def6;
consider j such that
A5: y = Class(R,j) by A2,EQREL_1:36;
A6: y = j/\/FI by A5,Def6;
take z = (i=>j)/\/FI;
A7: i"/\"(i=>j) [= j by FILTER_0:def 7;
(i"/\"(i=>j))"/\"Top I = i"/\"(i=>j);
then Top I [= (i"/\"(i=>j))=>j by A7,FILTER_0:def 7;
then (i"/\"(i=>j))=>j in FI by A1;
then (i"/\"(i=>j))/\/FI [= y by A6,Th16;
hence x"/\"z [= y by A4,Th15;
let t be Element of L;
consider k such that
A8: t = Class(R,k) by A2,EQREL_1:36;
A9: k/\/FI = t by A8,Def6;
assume
A10: x"/\"t [= y;
(i/\/FI)"/\"(k/\/FI) = (i"/\"k)/\/FI by Th15;
then (i"/\"k)=>j in FI by A4,A6,A9,A10,Th16;
then k=>(i=>j) in FI by Th17;
hence thesis by A9,Th16;
end;
end;
theorem
B/\/FB is B_Lattice
proof
set L = B/\/FB;
set R = equivalence_wrt FB;
A1: L is 0_Lattice by Th18;
A2: Bottom L = (Bottom B)/\/FB by Th18;
A3: Top L = (Top B)/\/FB by Th19;
reconsider L as 01_Lattice by A1;
A4: L is complemented
proof
let x be Element of L;
L = LattStr (#Class R, (the L_join of B)/\/R, (the L_meet of B)/\/R #)
by Def5;
then consider a being Element of B such that
A5: x = Class(R,a) by EQREL_1:36;
reconsider y = a`/\/FB as Element of L;
take y;
A6: x = a/\/FB by A5,Def6;
hence y"\/"x = (a`"\/"a)/\/FB by Th15
.= (Top B)/\/FB by LATTICES:21
.= Top L by A3;
hence x"\/"y = Top L;
thus y"/\"x = (a`"/\"a)/\/FB by A6,Th15
.= Bottom L by A2,LATTICES:20;
hence x"/\"y = Bottom L;
end;
thus thesis by A4;
end;
definition
let D1,D2 be set;
let f1 be BinOp of D1;
let f2 be BinOp of D2;
redefine func |:f1,f2:| -> BinOp of [:D1,D2:]; :: redefines |: (FUNCT_4, definition)
coherence
proof
D2 = {} implies [:D2,D2:] = {} by ZFMISC_1:90;
then
A1: dom f2 = [:D2,D2:] by FUNCT_2:def 1;
A2: rng f2 c= D2 by RELAT_1:def 19;
rng f1 c= D1 by RELAT_1:def 19;
then
A3: [:rng f1,rng f2:] c= [:D1,D2:] by A2,ZFMISC_1:96;
A4: rng |:f1,f2:| c= [:rng f1,rng f2:] by FUNCT_4:56;
D1 = {} implies [:D1,D1:] = {} by ZFMISC_1:90;
then dom f1 = [:D1,D1:] by FUNCT_2:def 1;
then dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by A1,FUNCT_4:58;
hence thesis by A3,A4,FUNCT_2:2,XBOOLE_1:1;
end;
end;
theorem Th21:
|:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)]
proof
A1: dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by FUNCT_2:def 1;
[[a1,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:];
hence thesis by A1,FUNCT_4:55;
end;
scheme
AuxCart1 { D1() -> non empty set, D2() -> non empty set, P[set] }: for d
being Element of [:D1(),D2():] holds P[d]
provided
A1: for d1 being Element of D1(), d2 being Element of D2() holds P[[d1, d2]]
proof
let d be Element of [:D1(),D2():];
ex d1 being Element of D1(), d2 being Element of D2() st d = [d1,d2] by
DOMAIN_1:1;
hence thesis by A1;
end;
scheme
AuxCart2 { D1() -> non empty set, D2() -> non empty set, P[set,set] }: for d
,d9 being Element of [:D1(),D2():] holds P[d,d9]
provided
A1: for d1,d19 being Element of D1(), d2,d29 being Element of D2() holds
P[[d1,d2],[d19,d29]]
proof
let d,d9 be Element of [:D1(),D2():];
A2: ex d19 being Element of D1(), d29 being Element of D2() st d9 = [d19,d29
] by DOMAIN_1:1;
ex d1 being Element of D1(), d2 being Element of D2() st d = [d1,d2] by
DOMAIN_1:1;
hence thesis by A1,A2;
end;
scheme
AuxCart3 { D1() -> non empty set, D2() -> non empty set, P[set,set,set] }:
for a,b,c being Element of [:D1(),D2():] holds P[a,b,c]
provided
A1: for a1,b1,c1 being Element of D1(), a2,b2,c2 being Element of D2()
holds P[[a1,a2],[b1,b2],[c1,c2]]
proof
let a,b,c be Element of [:D1(),D2():];
A2: ex b1 being Element of D1(), b2 being Element of D2() st b = [b1,b2] by
DOMAIN_1:1;
A3: ex c1 being Element of D1(), c2 being Element of D2() st c = [c1,c2] by
DOMAIN_1:1;
ex a1 being Element of D1(), a2 being Element of D2() st a = [a1,a2] by
DOMAIN_1:1;
hence thesis by A1,A2,A3;
end;
theorem Th22:
f1 is commutative & f2 is commutative iff |:f1,f2:| is commutative
proof
defpred P[set,set] means |:f1,f2:|.($1,$2) = |:f1,f2:|.($2,$1);
thus f1 is commutative & f2 is commutative implies |:f1,f2:| is commutative
proof
assume
A1: for a,b being Element of D1 holds f1.(a,b) = f1.(b,a);
assume
A2: for a,b being Element of D2 holds f2.(a,b) = f2.(b,a);
A3: for d1,d19 being Element of D1, d2,d29 being Element of D2 holds P[[d1
,d2],[d19,d29]]
proof
let a1,b1 be Element of D1, a2,b2 be Element of D2;
thus |:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)] by Th21
.= [f1.(b1,a1),f2.(a2,b2)] by A1
.= [f1.(b1,a1),f2.(b2,a2)] by A2
.= |:f1,f2:|.([b1,b2],[a1,a2]) by Th21;
end;
thus for a,b being Element of [:D1,D2:] holds P[a,b] from AuxCart2( A3);
end;
assume
A4: for a,b being Element of [:D1,D2:] holds |:f1,f2:|.(a,b) = |:f1,f2:|
.(b,a);
thus for a,b being Element of D1 holds f1.(a,b) = f1.(b,a)
proof
set a2 = the Element of D2;
let a1,b1;
[f1.(a1,b1),f2.(a2,a2)] = |:f1,f2:|.([a1,a2],[b1,a2]) by Th21
.= |:f1,f2:|.([b1,a2],[a1,a2]) by A4
.= [f1.(b1,a1),f2.(a2,a2)] by Th21;
hence thesis by XTUPLE_0:1;
end;
set a1 = the Element of D1;
let a2,b2;
[f1.(a1,a1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[a1,b2]) by Th21
.= |:f1,f2:|.([a1,b2],[a1,a2]) by A4
.= [f1.(a1,a1),f2.(b2,a2)] by Th21;
hence thesis by XTUPLE_0:1;
end;
theorem Th23:
f1 is associative & f2 is associative iff |:f1,f2:| is associative
proof
thus f1 is associative & f2 is associative implies |:f1,f2:| is associative
proof
defpred P[set,set,set] means |:f1,f2:|.($1,|:f1,f2:|.($2,$3)) = |:f1,f2:|.
(|:f1,f2:|.($1,$2),$3);
assume
A1: for a,b,c being Element of D1 holds f1.(a,f1.(b,c)) = f1.(f1.(a,b) ,c);
assume
A2: for a,b,c being Element of D2 holds f2.(a,f2.(b,c)) = f2.(f2.(a,b) ,c);
A3: now
let a1,b1,c1 be Element of D1, a2,b2,c2 be Element of D2;
|:f1,f2:|.([a1,a2],|:f1,f2:|.([b1,b2],[c1,c2])) = |:f1,f2:|.([a1,a2]
,[f1.(b1,c1),f2.(b2,c2)]) by Th21
.= [f1.(a1,f1.(b1,c1)),f2.(a2,f2.(b2,c2))] by Th21
.= [f1.(f1.(a1,b1),c1),f2.(a2,f2.(b2,c2))] by A1
.= [f1.(f1.(a1,b1),c1),f2.(f2.(a2,b2),c2)] by A2
.= |:f1,f2:|.([f1.(a1,b1),f2.(a2,b2)],[c1,c2]) by Th21
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[c1,c2]) by Th21;
hence P[[a1,a2],[b1,b2],[c1,c2]];
end;
thus for a,b,c being Element of [:D1,D2:] holds P[a,b,c] from AuxCart3(A3);
end;
assume
A4: for a,b,c being Element of [:D1,D2:] holds |:f1,f2:|.(a,|:f1,f2:|.(b
,c)) = |:f1,f2:|.(|:f1,f2:|.(a,b),c);
thus for a,b,c being Element of D1 holds f1.(a,f1.(b,c)) = f1.(f1.(a,b),c)
proof
set a2 = the Element of D2;
let a1,b1,c1;
[f1.(a1,f1.(b1,c1)), f2.(a2,f2.(a2,a2))] = |:f1,f2:|.([a1,a2],[f1.(b1,
c1),f2.(a2,a2)]) by Th21
.= |:f1,f2:|.([a1,a2],|:f1,f2:|.([b1,a2],[c1,a2])) by Th21
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[b1,a2]),[c1,a2]) by A4
.= |:f1,f2:|.([f1.(a1,b1),f2.(a2,a2)],[c1,a2]) by Th21
.= [f1.(f1.(a1,b1),c1), f2.(f2.(a2,a2),a2)] by Th21;
hence thesis by XTUPLE_0:1;
end;
set a1 = the Element of D1;
let a2,b2,c2;
[f1.(a1,f1.(a1,a1)), f2.(a2,f2.(b2,c2))] = |:f1,f2:|.([a1,a2],[f1.(a1,a1
),f2.(b2,c2)]) by Th21
.= |:f1,f2:|.([a1,a2],|:f1,f2:|.([a1,b2],[a1,c2])) by Th21
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[a1,b2]),[a1,c2]) by A4
.= |:f1,f2:|.([f1.(a1,a1),f2.(a2,b2)],[a1,c2]) by Th21
.= [f1.(f1.(a1,a1),a1), f2.(f2.(a2,b2),c2)] by Th21;
hence thesis by XTUPLE_0:1;
end;
theorem Th24:
a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 iff [a1,a2
] is_a_left_unity_wrt |:f1,f2:|
proof
thus a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 implies [a1,a2]
is_a_left_unity_wrt |:f1,f2:|
proof
defpred P[set] means |:f1,f2:|.([a1,a2],$1) = $1;
assume
A1: f1.(a1,b1) = b1;
assume
A2: f2.(a2,b2) = b2;
A3: now
let b1,b2;
|:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)] by Th21
.= [b1,f2.(a2,b2)] by A1
.= [b1,b2] by A2;
hence P[[b1,b2]];
end;
thus for a being Element of [:D1,D2:] holds P[a] from AuxCart1(A3);
end;
assume
A4: for a being Element of [:D1,D2:] holds |:f1,f2:|.([a1,a2],a) = a;
thus f1.(a1,b1) = b1
proof
set b2 = the Element of D2;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th21
.= [b1,b2] by A4;
hence thesis by XTUPLE_0:1;
end;
set b1 = the Element of D1;
let b2;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th21
.= [b1,b2] by A4;
hence thesis by XTUPLE_0:1;
end;
theorem Th25:
a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 iff [a1,
a2] is_a_right_unity_wrt |:f1,f2:|
proof
thus a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 implies [a1,a2]
is_a_right_unity_wrt |:f1,f2:|
proof
defpred P[set] means |:f1,f2:|.($1,[a1,a2]) = $1;
assume
A1: f1.(b1,a1) = b1;
assume
A2: f2.(b2,a2) = b2;
A3: now
let b1,b2;
|:f1,f2:|.([b1,b2],[a1,a2]) = [f1.(b1,a1),f2.(b2,a2)] by Th21
.= [b1,f2.(b2,a2)] by A1
.= [b1,b2] by A2;
hence P[[b1,b2]];
end;
thus for a being Element of [:D1,D2:] holds P[a] from AuxCart1(A3);
end;
assume
A4: for a being Element of [:D1,D2:] holds |:f1,f2:|.(a,[a1,a2]) = a;
thus f1.(b1,a1) = b1
proof
set b2 = the Element of D2;
[f1.(b1,a1),f2.(b2,a2)] = |:f1,f2:|.([b1,b2],[a1,a2]) by Th21
.= [b1,b2] by A4;
hence thesis by XTUPLE_0:1;
end;
set b1 = the Element of D1;
let b2;
[f1.(b1,a1),f2.(b2,a2)] = |:f1,f2:|.([b1,b2],[a1,a2]) by Th21
.= [b1,b2] by A4;
hence thesis by XTUPLE_0:1;
end;
theorem
a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 iff [a1,a2] is_a_unity_wrt
|:f1,f2:|
by Th24,Th25;
theorem Th27:
f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2
iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:|
proof
thus f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 implies
|:f1,f2:| is_left_distributive_wrt |:g1,g2:|
proof
defpred P[set,set,set] means |:f1,f2:|.($1,|:g1,g2:|.($2,$3)) = |:g1,g2:|.
(|:f1,f2:|.($1,$2),|:f1,f2:|.($1,$3));
assume
A1: for a1,b1,c1 holds f1.(a1,g1.(b1,c1)) = g1.(f1.(a1,b1),f1.(a1,c1));
assume
A2: for a2,b2,c2 holds f2.(a2,g2.(b2,c2)) = g2.(f2.(a2,b2),f2.(a2,c2));
A3: now
let a1,b1,c1, a2,b2,c2;
|:f1,f2:|.([a1,a2],|:g1,g2:|.([b1,b2],[c1,c2])) = |:f1,f2:|.([a1,a2]
,[g1.(b1,c1),g2.(b2,c2)]) by Th21
.= [f1.(a1,g1.(b1,c1)),f2.(a2,g2.(b2,c2))] by Th21
.= [g1.(f1.(a1,b1),f1.(a1,c1)),f2.(a2,g2.(b2,c2))] by A1
.= [g1.(f1.(a1,b1),f1.(a1,c1)),g2.(f2.(a2,b2),f2.(a2,c2))] by A2
.= |:g1,g2:|.([f1.(a1,b1),f2.(a2,b2)],[f1.(a1,c1),f2.(a2,c2)]) by Th21
.= |:g1,g2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[f1.(a1,c1),f2.(a2,c2)])
by Th21
.= |:g1,g2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),|:f1,f2:|.([a1,a2],[c1,c2]
)) by Th21;
hence P[[a1,a2],[b1,b2],[c1,c2]];
end;
thus for a,b,c being Element of [:D1,D2:] holds P[a,b,c] from AuxCart3(A3);
end;
assume
A4: for a,b,c being Element of [:D1,D2:] holds |:f1,f2:|.(a,|:g1,g2:|.(b
,c)) = |:g1,g2:|.(|:f1,f2:|.(a,b),|:f1,f2:|.(a,c));
A5: now
let a1,b1,c1, a2,b2,c2;
thus [f1.(a1,g1.(b1,c1)),f2.(a2,g2.(b2,c2))] = |:f1,f2:|.([a1,a2],[g1.(b1,
c1),g2.(b2,c2)]) by Th21
.= |:f1,f2:|.([a1,a2],|:g1,g2:|.([b1,b2],[c1,c2])) by Th21
.= |:g1,g2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),|:f1,f2:|.([a1,a2],[c1,c2]))
by A4
.= |:g1,g2:|.([f1.(a1,b1),f2.(a2,b2)],|:f1,f2:|.([a1,a2],[c1,c2])) by
Th21
.= |:g1,g2:|.([f1.(a1,b1),f2.(a2,b2)],[f1.(a1,c1),f2.(a2,c2)]) by Th21
.= [g1.(f1.(a1,b1),f1.(a1,c1)),g2.(f2.(a2,b2),f2.(a2,c2))] by Th21;
end;
thus for a1,b1,c1 holds f1.(a1,g1.(b1,c1)) = g1.(f1.(a1,b1),f1.(a1,c1))
proof
set a2 = the Element of D2;
let a1,b1,c1;
[f1.(a1,g1.(b1,c1)),f2.(a2,g2.(a2,a2))] = [g1.(f1.(a1,b1),f1.(a1,c1)),
g2.(f2.(a2,a2),f2.(a2,a2))] by A5;
hence thesis by XTUPLE_0:1;
end;
set a1 = the Element of D1;
let a2,b2,c2;
[f1.(a1,g1.(a1,a1)),f2.(a2,g2.(b2,c2))] = [g1.(f1.(a1,a1),f1.(a1,a1)),g2
.(f2.(a2,b2),f2.(a2,c2))] by A5;
hence thesis by XTUPLE_0:1;
end;
theorem Th28:
f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt
g2 iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:|
proof
thus f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2
implies |:f1,f2:| is_right_distributive_wrt |:g1,g2:|
proof
defpred P[set,set,set] means |:f1,f2:|.(|:g1,g2:|.($2,$3),$1) = |:g1,g2:|.
(|:f1,f2:|.($2,$1),|:f1,f2:|.($3,$1));
assume
A1: for b1,c1,a1 holds f1.(g1.(b1,c1),a1) = g1.(f1.(b1,a1),f1.(c1,a1));
assume
A2: for b2,c2,a2 holds f2.(g2.(b2,c2),a2) = g2.(f2.(b2,a2),f2.(c2,a2));
A3: now
let a1,b1,c1, a2,b2,c2;
|:f1,f2:|.(|:g1,g2:|.([b1,b2],[c1,c2]),[a1,a2]) = |:f1,f2:|.([g1.(b1
,c1),g2.(b2,c2)],[a1,a2]) by Th21
.= [f1.(g1.(b1,c1),a1),f2.(g2.(b2,c2),a2)] by Th21
.= [g1.(f1.(b1,a1),f1.(c1,a1)),f2.(g2.(b2,c2),a2)] by A1
.= [g1.(f1.(b1,a1),f1.(c1,a1)),g2.(f2.(b2,a2),f2.(c2,a2))] by A2
.= |:g1,g2:|.([f1.(b1,a1),f2.(b2,a2)],[f1.(c1,a1),f2.(c2,a2)]) by Th21
.= |:g1,g2:|.(|:f1,f2:|.([b1,b2],[a1,a2]),[f1.(c1,a1),f2.(c2,a2)])
by Th21
.= |:g1,g2:|.(|:f1,f2:|.([b1,b2],[a1,a2]),|:f1,f2:|.([c1,c2],[a1,a2]
)) by Th21;
hence P[[a1,a2],[b1,b2],[c1,c2]];
end;
for a,b,c being Element of [:D1,D2:] holds P[a,b,c] from AuxCart3( A3);
then for b,c,a being Element of [:D1,D2:] holds P[a,b,c];
hence thesis;
end;
assume
A4: for b,c,a being Element of [:D1,D2:] holds |:f1,f2:|.(|:g1,g2:|.(b,c
),a) = |:g1,g2:|.(|:f1,f2:|.(b,a),|:f1,f2:|.(c,a));
A5: now
let a1,b1,c1, a2,b2,c2;
thus [f1.(g1.(b1,c1),a1),f2.(g2.(b2,c2),a2)] = |:f1,f2:|.([g1.(b1,c1),g2.(
b2,c2)],[a1,a2]) by Th21
.= |:f1,f2:|.(|:g1,g2:|.([b1,b2],[c1,c2]),[a1,a2]) by Th21
.= |:g1,g2:|.(|:f1,f2:|.([b1,b2],[a1,a2]),|:f1,f2:|.([c1,c2],[a1,a2]))
by A4
.= |:g1,g2:|.([f1.(b1,a1),f2.(b2,a2)],|:f1,f2:|.([c1,c2],[a1,a2])) by
Th21
.= |:g1,g2:|.([f1.(b1,a1),f2.(b2,a2)],[f1.(c1,a1),f2.(c2,a2)]) by Th21
.= [g1.(f1.(b1,a1),f1.(c1,a1)),g2.(f2.(b2,a2),f2.(c2,a2))] by Th21;
end;
thus for b1,c1,a1 holds f1.(g1.(b1,c1),a1) = g1.(f1.(b1,a1),f1.(c1,a1))
proof
set a2 = the Element of D2;
let b1,c1,a1;
[f1.(g1.(b1,c1),a1),f2.(g2.(a2,a2),a2)] = [g1.(f1.(b1,a1),f1.(c1,a1)),
g2.(f2.(a2,a2),f2.(a2,a2))] by A5;
hence thesis by XTUPLE_0:1;
end;
set a1 = the Element of D1;
let b2,c2,a2;
[f1.(g1.(a1,a1),a1),f2.(g2.(b2,c2),a2)] = [g1.(f1.(a1,a1),f1.(a1,a1)),
g2.(f2.(b2,a2),f2.(c2,a2))] by A5;
hence thesis by XTUPLE_0:1;
end;
theorem Th29:
f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 iff |:f1,
f2:| is_distributive_wrt |:g1,g2:|
by Th27,Th28;
theorem Th30:
f1 absorbs g1 & f2 absorbs g2 iff |:f1,f2:| absorbs |:g1,g2:|
proof
defpred P[set,set] means |:f1,f2:|.($1,|:g1,g2:|.($1,$2)) = $1;
thus f1 absorbs g1 & f2 absorbs g2 implies |:f1,f2:| absorbs |:g1,g2:|
proof
assume
A1: for a1,b1 holds f1.(a1,g1.(a1,b1)) = a1;
assume
A2: for a2,b2 holds f2.(a2,g2.(a2,b2)) = a2;
A3: for d1,d19 being Element of D1, d2,d29 being Element of D2 holds P[[d1
,d2],[d19,d29]]
proof
let a1,b1, a2,b2;
thus |:f1,f2:|.([a1,a2],|:g1,g2:|.([a1,a2],[b1,b2])) = |:f1,f2:|.([a1,a2
],[g1.(a1,b1),g2.(a2,b2)]) by Th21
.= [f1.(a1,g1.(a1,b1)),f2.(a2,g2.(a2,b2))] by Th21
.= [a1,f2.(a2,g2.(a2,b2))] by A1
.= [a1,a2] by A2;
end;
thus for a,b being Element of [:D1,D2:] holds P[a,b] from AuxCart2( A3);
end;
assume
A4: for a,b being Element of [:D1,D2:] holds |:f1,f2:|.(a,|:g1,g2:|.(a,b
)) = a;
thus for a1,b1 holds f1.(a1,g1.(a1,b1)) = a1
proof
set a2 = the Element of D2;
let a1,b1;
[a1,a2] = |:f1,f2:|.([a1,a2],|:g1,g2:|.([a1,a2],[b1,a2])) by A4
.= |:f1,f2:|.([a1,a2],[g1.(a1,b1),g2.(a2,a2)]) by Th21
.= [f1.(a1,g1.(a1,b1)),f2.(a2,g2.(a2,a2))] by Th21;
hence thesis by XTUPLE_0:1;
end;
set a1 = the Element of D1;
let a2,b2;
[a1,a2] = |:f1,f2:|.([a1,a2],|:g1,g2:|.([a1,a2],[a1,b2])) by A4
.= |:f1,f2:|.([a1,a2],[g1.(a1,a1),g2.(a2,b2)]) by Th21
.= [f1.(a1,g1.(a1,a1)),f2.(a2,g2.(a2,b2))] by Th21;
hence thesis by XTUPLE_0:1;
end;
definition
let L1,L2 be non empty LattStr;
func [:L1,L2:] -> strict LattStr equals
LattStr (#[: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:|#);
correctness;
end;
registration
let L1,L2 be non empty LattStr;
cluster [:L1,L2:] -> non empty;
coherence;
end;
definition
let L be Lattice;
func LattRel L -> Relation equals
{ [p,q] where p is Element of L, q is
Element of L: p [= q };
coherence
proof
now
let x be object;
assume x in { [p,q] where p is Element of L, q is Element of L: p [= q };
then ex p,q being Element of L st x = [p,q] & p [= q;
hence ex x1,x2 being object st x = [x1,x2];
end;
hence thesis by RELAT_1:def 1;
end;
end;
theorem Th31:
[p,q] in LattRel L iff p [= q
proof
thus [p,q] in LattRel L implies p [= q
proof
assume [p,q] in LattRel L;
then consider r,s such that
A1: [p,q] = [r,s] and
A2: r [= s;
thus thesis by A1,A2,XTUPLE_0:1;
end;
thus thesis;
end;
theorem Th32:
dom LattRel L = the carrier of L & rng LattRel L = the carrier
of L & field LattRel L = the carrier of L
proof
now
let x be object;
thus x in the carrier of L implies ex y being object st [x,y] in LattRel L
proof
assume x in the carrier of L;
then reconsider p = x as Element of L;
[p,p] in LattRel L;
hence thesis;
end;
given y being object such that
A1: [x,y] in LattRel L;
consider p,q such that
A2: [x,y] = [p,q] and
p [= q by A1;
x = p by A2,XTUPLE_0:1;
hence x in the carrier of L;
end;
hence
A3: dom LattRel L = the carrier of L by XTUPLE_0:def 12;
now
let x be object;
thus x in the carrier of L implies ex y being object st [y,x] in LattRel L
proof
assume x in the carrier of L;
then reconsider p = x as Element of L;
[p,p] in LattRel L;
hence thesis;
end;
given y being object such that
A4: [y,x] in LattRel L;
consider p,q such that
A5: [y,x] = [p,q] and
p [= q by A4;
x = q by A5,XTUPLE_0:1;
hence x in the carrier of L;
end;
hence rng LattRel L = the carrier of L by XTUPLE_0:def 13;
hence field LattRel L = (the carrier of L) \/ the carrier of L by A3,
RELAT_1:def 6
.= the carrier of L;
end;
definition
let L1,L2 be Lattice;
pred L1,L2 are_isomorphic means
LattRel L1, LattRel L2 are_isomorphic;
reflexivity by WELLORD1:38;
symmetry by WELLORD1:40;
end;
registration
let L1,L2 be Lattice;
cluster [:L1,L2:] -> Lattice-like;
coherence
proof
reconsider LL = LattStr (#[: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:|#) as
non empty LattStr;
A1: join(L2) absorbs meet(L2) by LATTICE2:26;
join(L1) absorbs meet(L1) by LATTICE2:26;
then
A2: join(LL) absorbs meet(LL) by A1,Th30;
A3: join(LL) is associative by Th23;
A4: meet(L2) absorbs join(L2) by LATTICE2:27;
meet(L1) absorbs join(L1) by LATTICE2:27;
then
A5: meet(LL) absorbs join(LL) by A4,Th30;
A6: meet(LL) is commutative by Th22;
A7: meet(LL) is associative by Th23;
join(LL) is commutative by Th22;
hence thesis by A3,A6,A7,A2,A5,LATTICE2:11;
end;
end;
theorem
for L1,L2,L3 being Lattice st L1,L2 are_isomorphic & L2,L3
are_isomorphic holds L1,L3 are_isomorphic
by WELLORD1:42;
theorem
for L1,L2 being non empty LattStr st [:L1,L2:] is Lattice holds L1 is
Lattice & L2 is Lattice
proof
let L1,L2 be non empty LattStr such that
A1: [:L1,L2:] is Lattice;
A2: join(L1) is associative by A1,Th23;
A3: meet(L2) is associative by A1,Th23;
A4: meet(L2) is commutative by A1,Th22;
reconsider LL = LattStr (#[:the carrier of L1, the carrier of L2:], |:join(
L1), join(L2):|, |:meet(L1),meet(L2):|#) as non empty LattStr;
A5: join(LL) absorbs meet(LL) by A1,LATTICE2:26;
then
A6: join(L1) absorbs meet(L1) by Th30;
A7: join(L2) is associative by A1,Th23;
A8: join(L2) is commutative by A1,Th22;
A9: meet(L1) is associative by A1,Th23;
A10: meet(L1) is commutative by A1,Th22;
A11: meet(LL) absorbs join(LL) by A1,LATTICE2:27;
then
A12: meet(L1) absorbs join(L1) by Th30;
A13: meet(L2) absorbs join(L2) by A11,Th30;
A14: join(L2) absorbs meet(L2) by A5,Th30;
join(L1) is commutative by A1,Th22;
hence thesis by A2,A10,A9,A6,A12,A8,A7,A4,A3,A14,A13,LATTICE2:11;
end;
definition
let L1,L2 be Lattice;
let a be Element of L1, b be Element of L2;
redefine func [a,b] -> Element of [:L1,L2:]; :: redefines [ (TARSKI, definition)
coherence
proof
[a,b] is Element of [:the carrier of L1, the carrier of L2:];
hence thesis;
end;
end;
theorem
[p1,p2] "\/" [q1,q2] = [p1"\/"q1,p2"\/"q2] & [p1,p2] "/\" [q1,q2] = [
p1"/\"q1,p2"/\"q2] by Th21;
theorem Th36:
[p1,p2] [= [q1,q2] iff p1 [= q1 & p2 [= q2
proof
thus [p1,p2] [= [q1,q2] implies p1 [= q1 & p2 [= q2
proof
assume [p1,p2] "\/" [q1,q2] = [q1,q2];
then [p1"\/"q1,p2"\/"q2] = [q1,q2] by Th21;
hence p1"\/"q1 = q1 & p2"\/"q2 = q2 by XTUPLE_0:1;
end;
assume that
A1: p1"\/"q1 = q1 and
A2: p2"\/"q2 = q2;
thus [p1,p2] "\/" [q1,q2] = [q1,q2] by A1,A2,Th21;
end;
theorem
L1 is modular & L2 is modular iff [:L1,L2:] is modular
proof
thus L1 is modular & L2 is modular implies [:L1,L2:] is modular
proof
assume
A1: for p1,q1,r1 st p1 [= r1 holds p1"\/"(q1"/\"r1) = (p1"\/"q1)"/\"r1;
assume
A2: for p2,q2,r2 st p2 [= r2 holds p2"\/"(q2"/\"r2) = (p2"\/"q2)"/\"r2;
let a,b,c be Element of [:L1,L2:] such that
A3: a [= c;
consider q1,q2 such that
A4: b = [q1,q2] by DOMAIN_1:1;
consider p1,p2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
consider r1,r2 such that
A6: c = [r1,r2] by DOMAIN_1:1;
A7: p2 [= r2 by A3,A5,A6,Th36;
A8: p1 [= r1 by A3,A5,A6,Th36;
thus a"\/"(b"/\"c) = a"\/"([q1"/\"r1,q2"/\"r2]) by A4,A6,Th21
.= [p1"\/"(q1"/\"r1),p2"\/"(q2"/\"r2)] by A5,Th21
.= [(p1"\/"q1)"/\"r1,p2"\/"(q2"/\"r2)] by A1,A8
.= [(p1"\/"q1)"/\"r1,(p2"\/"q2)"/\"r2] by A2,A7
.= [p1"\/"q1,p2"\/"q2]"/\"c by A6,Th21
.= (a"\/"b)"/\"c by A5,A4,Th21;
end;
assume
A9: for a,b,c be Element of [:L1,L2:] st a [= c holds a"\/"(b"/\"c) = (a
"\/"b)"/\"c;
thus L1 is modular
proof
set p2 = the Element of L2;
let p1,q1,r1;
assume p1 [= r1;
then [p1,p2] [= [r1,p2] by Th36;
then
A10: [p1,p2]"\/"([q1,p2]"/\"[r1,p2]) = ([p1,p2]"\/"[q1,p2])"/\"[r1,p2] by A9;
A11: [p1,p2]"\/"[q1,p2] = [p1"\/"q1,p2"\/"p2] by Th21;
A12: [p1"\/"q1,p2"\/"p2]"/\"[r1,p2] = [(p1"\/"q1)"/\"r1,(p2"\/"p2)"/\" p2]
by Th21;
A13: [p1,p2]"\/"[q1"/\"r1,p2"/\"p2] = [p1"\/"(q1"/\"r1),p2"\/"(p2"/\"p2)]
by Th21;
[q1,p2]"/\"[r1,p2] = [q1"/\"r1,p2"/\"p2] by Th21;
hence thesis by A10,A11,A13,A12,XTUPLE_0:1;
end;
set p1 = the Element of L1;
let p2,q2,r2;
assume p2 [= r2;
then [p1,p2] [= [p1,r2] by Th36;
then
A14: [p1,p2]"\/"([p1,q2]"/\"[p1,r2]) = ([p1,p2]"\/"[p1,q2])"/\"[p1,r2] by A9;
A15: [p1,p2]"\/"[p1,q2] = [p1"\/"p1,p2"\/"q2] by Th21;
A16: [p1"\/"p1,p2"\/"q2]"/\"[p1,r2] = [(p1"\/"p1)"/\"p1,(p2"\/"q2)"/\" r2]
by Th21;
A17: [p1,p2]"\/"[p1"/\"p1,q2"/\"r2] = [p1"\/"(p1"/\"p1),p2"\/"(q2"/\"r2)] by
Th21;
[p1,q2]"/\"[p1,r2] = [p1"/\"p1,q2"/\"r2] by Th21;
hence thesis by A14,A15,A17,A16,XTUPLE_0:1;
end;
theorem Th38:
L1 is D_Lattice & L2 is D_Lattice iff [:L1,L2:] is D_Lattice
proof
thus L1 is D_Lattice & L2 is D_Lattice implies [:L1,L2:] is D_Lattice
proof
assume that
A1: L1 is D_Lattice and
A2: L2 is D_Lattice;
A3: join(L2) is_distributive_wrt meet(L2) by A2,LATTICE2:21;
join(L1) is_distributive_wrt meet(L1) by A1,LATTICE2:21;
then |:join(L1),join(L2):| is_distributive_wrt |:meet(L1),meet(L2):| by A3
,Th29;
hence thesis by LATTICE2:22;
end;
assume [:L1,L2:] is D_Lattice;
then
A4: join([:L1,L2:]) is_distributive_wrt meet([:L1,L2:]) by LATTICE2:21;
then
A5: join(L2) is_distributive_wrt meet(L2) by Th29;
join(L1) is_distributive_wrt meet(L1) by A4,Th29;
hence thesis by A5,LATTICE2:22;
end;
theorem Th39:
L1 is lower-bounded & L2 is lower-bounded iff [:L1,L2:] is lower-bounded
proof
thus L1 is lower-bounded & L2 is lower-bounded implies [:L1,L2:] is
lower-bounded
proof
given p1 such that
A1: p1"/\"q1 = p1 & q1"/\"p1 = p1;
given p2 such that
A2: p2"/\"q2 = p2 & q2"/\"p2 = p2;
take a = [p1,p2];
let b be Element of [:L1,L2:];
consider q1,q2 such that
A3: b = [q1,q2] by DOMAIN_1:1;
thus a"/\"b = [p1"/\"q1,p2"/\"q2] by A3,Th21
.= [p1,p2"/\" q2] by A1
.= a by A2;
hence b"/\"a = a;
end;
given a being Element of [:L1,L2:] such that
A4: for b being Element of [:L1,L2:] holds a"/\"b = a & b"/\"a = a;
consider p1,p2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
thus L1 is lower-bounded
proof
set q2 = the Element of L2;
take p1;
let q1;
a = a"/\"[q1,q2] by A4
.= [p1"/\"q1,p2"/\"q2] by A5,Th21;
hence thesis by A5,XTUPLE_0:1;
end;
set q1 = the Element of L1;
take p2;
let q2;
a = a"/\"[q1,q2] by A4
.= [p1"/\"q1,p2"/\"q2] by A5,Th21;
hence thesis by A5,XTUPLE_0:1;
end;
theorem Th40:
L1 is upper-bounded & L2 is upper-bounded iff [:L1,L2:] is upper-bounded
proof
thus L1 is upper-bounded & L2 is upper-bounded implies [:L1,L2:] is
upper-bounded
proof
given p1 such that
A1: p1"\/"q1 = p1 & q1"\/"p1 = p1;
given p2 such that
A2: p2"\/"q2 = p2 & q2"\/"p2 = p2;
take a = [p1,p2];
let b be Element of [:L1,L2:];
consider q1,q2 such that
A3: b = [q1,q2] by DOMAIN_1:1;
thus a"\/"b = [p1"\/"q1,p2"\/"q2] by A3,Th21
.= [p1,p2"\/" q2] by A1
.= a by A2;
hence b"\/"a = a;
end;
given a being Element of [:L1,L2:] such that
A4: for b being Element of [:L1,L2:] holds a"\/"b = a & b"\/"a = a;
consider p1,p2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
thus L1 is upper-bounded
proof
set q2 = the Element of L2;
take p1;
let q1;
a = a"\/"[q1,q2] by A4
.= [p1"\/"q1,p2"\/"q2] by A5,Th21;
hence thesis by A5,XTUPLE_0:1;
end;
set q1 = the Element of L1;
take p2;
let q2;
a = a"\/"[q1,q2] by A4
.= [p1"\/"q1,p2"\/"q2] by A5,Th21;
hence thesis by A5,XTUPLE_0:1;
end;
theorem Th41:
L1 is bounded & L2 is bounded iff [:L1,L2:] is bounded
by Th39,Th40;
theorem Th42:
L1 is 0_Lattice & L2 is 0_Lattice implies Bottom [:L1,L2:] = [
Bottom L1, Bottom L2]
proof
assume that
A1: L1 is 0_Lattice and
A2: L2 is 0_Lattice;
A3: now
let a be Element of [:L1,L2:];
consider p1,p2 such that
A4: a = [p1,p2] by DOMAIN_1:1;
thus [Bottom L1,Bottom L2]"/\"a = [Bottom L1"/\"p1,Bottom L2"/\"p2] by A4
,Th21
.= [Bottom L1,Bottom L2"/\" p2] by A1
.= [Bottom L1,Bottom L2] by A2;
hence a"/\"[Bottom L1,Bottom L2]=[Bottom L1,Bottom L2];
end;
[:L1,L2:] is lower-bounded by A1,A2,Th39;
hence thesis by A3,LATTICES:def 16;
end;
theorem Th43:
L1 is 1_Lattice & L2 is 1_Lattice implies Top [:L1,L2:] = [Top L1,Top L2]
proof
assume that
A1: L1 is 1_Lattice and
A2: L2 is 1_Lattice;
A3: now
let a be Element of [:L1,L2:];
consider p1,p2 such that
A4: a = [p1,p2] by DOMAIN_1:1;
thus [Top L1,Top L2]"\/"a = [Top L1"\/"p1,Top L2"\/"p2] by A4,Th21
.= [ Top L1,Top L2"\/" p2] by A1
.= [Top L1,Top L2] by A2;
hence a"\/"[Top L1,Top L2] = [Top L1,Top L2];
end;
[:L1,L2:] is upper-bounded by A1,A2,Th40;
hence thesis by A3,LATTICES:def 17;
end;
theorem Th44:
L1 is 01_Lattice & L2 is 01_Lattice implies (p1
is_a_complement_of q1 & p2 is_a_complement_of q2 iff [p1,p2] is_a_complement_of
[q1,q2])
proof
assume that
A1: L1 is 01_Lattice and
A2: L2 is 01_Lattice;
thus p1 is_a_complement_of q1 & p2 is_a_complement_of q2 implies [p1,p2]
is_a_complement_of [q1,q2]
proof
assume that
A3: p1 is_a_complement_of q1 and
A4: p2 is_a_complement_of q2;
A5: p2"\/"q2 = Top L2 by A4;
p1"\/"q1 = Top L1 by A3;
hence [p1,p2]"\/"[q1,q2] = [Top L1,Top L2] by A5,Th21
.= Top [:L1,L2:] by A1,A2,Th43;
hence [q1,q2]"\/"[p1,p2] = Top [:L1,L2:];
A6: p2"/\"q2 = Bottom L2 by A4;
p1"/\"q1 = Bottom L1 by A3;
hence [p1,p2]"/\"[q1,q2] = [Bottom L1,Bottom L2] by A6,Th21
.= Bottom [:L1,L2:] by A1,A2,Th42;
hence [q1,q2]"/\"[p1,p2] = Bottom [:L1,L2:];
end;
assume
A7: [p1,p2] is_a_complement_of [q1,q2];
then
A8: [p1,p2]"/\"[q1,q2] = Bottom [: L1,L2:];
[Bottom L1,Bottom L2] = Bottom [:L1,L2:] by A1,A2,Th42;
then
A9: [p1"/\"q1,p2"/\"q2] = [Bottom L1,Bottom L2] by A8,Th21;
then
A10: p1"/\"q1 = Bottom L1 by XTUPLE_0:1;
A11: [p1,p2]"\/"[q1,q2] = Top [:L1,L2:] by A7;
A12: p2"/\"q2 = Bottom L2 by A9,XTUPLE_0:1;
A13: p1"\/"q1 = q1"\/"p1 & p1"/\"q1 = q1"/\"p1;
[Top L1,Top L2] = Top [:L1,L2:] by A1,A2,Th43;
then
A14: [Top L1,Top L2] = [p1"\/"q1,p2"\/"q2] by A11,Th21;
then p1"\/"q1 = Top L1 by XTUPLE_0:1;
hence p1 is_a_complement_of q1 by A10,A13;
A15: p2"\/"q2 = q2"\/"p2 & p2"/\"q2 = q2"/\"p2;
p2"\/"q2 = Top L2 by A14,XTUPLE_0:1;
hence thesis by A12,A15;
end;
theorem Th45:
L1 is C_Lattice & L2 is C_Lattice iff [:L1,L2:] is C_Lattice
proof
thus L1 is C_Lattice & L2 is C_Lattice implies [:L1,L2:] is C_Lattice
proof
assume that
A1: L1 is C_Lattice and
A2: L2 is C_Lattice;
reconsider L = [:L1,L2:] as 01_Lattice by A1,A2,Th41;
L is complemented
proof
let a be Element of L;
consider p1,p2 such that
A3: a = [p1,p2] by DOMAIN_1:1;
consider q1 such that
A4: q1 is_a_complement_of p1 by A1,LATTICES:def 19;
consider q2 such that
A5: q2 is_a_complement_of p2 by A2,LATTICES:def 19;
reconsider b = [q1,q2] as Element of L;
take b;
thus thesis by A1,A2,A3,A4,A5,Th44;
end;
hence thesis;
end;
assume
A6: [:L1,L2:] is C_Lattice;
then reconsider C1 = L1, C2 = L2 as 01_Lattice by Th41;
C1 is complemented
proof
set p29 = the Element of C2;
let p19 be Element of C1;
reconsider p1 = p19 as Element of L1;
reconsider p2 = p29 as Element of L2;
consider b being Element of [:L1,L2:] such that
A7: b is_a_complement_of [p1,p2] by A6,LATTICES:def 19;
consider q1,q2 such that
A8: b = [q1,q2] by DOMAIN_1:1;
reconsider q19 = q1 as Element of C1;
take q19;
thus thesis by A7,A8,Th44;
end;
hence L1 is C_Lattice;
C2 is complemented
proof
set p19 = the Element of C1;
let p29 be Element of C2;
reconsider p1 = p19 as Element of L1;
reconsider p2 = p29 as Element of L2;
consider b being Element of [:L1,L2:] such that
A9: b is_a_complement_of [p1,p2] by A6,LATTICES:def 19;
consider q1,q2 such that
A10: b = [q1,q2] by DOMAIN_1:1;
reconsider q29 = q2 as Element of C2;
take q29;
thus thesis by A9,A10,Th44;
end;
hence thesis;
end;
theorem
L1 is B_Lattice & L2 is B_Lattice iff [:L1,L2:] is B_Lattice
proof
A1: [:L1,L2:] is D_Lattice iff L1 is D_Lattice & L2 is D_Lattice by Th38;
[:L1,L2:] is C_Lattice iff L1 is C_Lattice & L2 is C_Lattice by Th45;
hence thesis by A1;
end;
theorem
L1 is implicative & L2 is implicative iff [:L1,L2:] is implicative
proof
thus L1 is implicative & L2 is implicative implies [:L1,L2:] is implicative
proof
assume
A1: for p1,q1 ex r1 st p1"/\"r1 [= q1 & for s1 st p1"/\"s1 [= q1 holds
s1 [= r1;
assume
A2: for p2,q2 ex r2 st p2"/\"r2 [= q2 & for s2 st p2"/\"s2 [= q2 holds
s2 [= r2;
let a,b be Element of [:L1,L2:];
consider p1,p2 such that
A3: a = [p1,p2] by DOMAIN_1:1;
consider q1,q2 such that
A4: b = [q1,q2] by DOMAIN_1:1;
consider r2 such that
A5: p2"/\"r2 [= q2 and
A6: for s2 st p2"/\"s2 [= q2 holds s2 [= r2 by A2;
consider r1 such that
A7: p1"/\"r1 [= q1 and
A8: for s1 st p1"/\"s1 [= q1 holds s1 [= r1 by A1;
take [r1,r2];
a"/\"[r1,r2] = [p1"/\"r1,p2"/\"r2] by A3,Th21;
hence a"/\"[r1,r2] [= b by A4,A7,A5,Th36;
let d be Element of [:L1,L2:];
consider s1,s2 such that
A9: d = [s1,s2] by DOMAIN_1:1;
assume a"/\"d [= b;
then
A10: [p1"/\"s1,p2"/\"s2] [= b by A3,A9,Th21;
then p2"/\"s2 [= q2 by A4,Th36;
then
A11: s2 [= r2 by A6;
p1"/\"s1 [= q1 by A4,A10,Th36;
then s1 [= r1 by A8;
hence d [= [r1,r2] by A9,A11,Th36;
end;
assume
A12: for a,b being Element of [:L1,L2:] ex c being Element of [:L1,L2:]
st a"/\"c [= b & for d being Element of [:L1,L2:] st a"/\" d [= b holds d [= c;
thus for p1,q1 ex r1 st p1"/\"r1 [= q1 & for s1 st p1"/\"s1 [= q1 holds s1
[= r1
proof
set p2 = the Element of L2;
let p1,q1;
consider c being Element of [:L1,L2:] such that
A13: [p1,p2]"/\"c [= [q1,p2] and
A14: for d being Element of [:L1,L2:] st [p1,p2]"/\"d [= [q1,p2] holds
d [= c by A12;
consider r1,r2 such that
A15: c = [r1,r2] by DOMAIN_1:1;
take r1;
A16: [p1,p2]"/\"c = [p1"/\"r1,p2"/\"r2] by A15,Th21;
hence p1"/\"r1 [= q1 by A13,Th36;
let s1;
assume
A17: p1"/\"s1 [= q1;
p2"/\"r2 [= p2 by A13,A16,Th36;
then [p1"/\"s1,p2"/\"r2] [= [q1,p2] by A17,Th36;
then [p1,p2]"/\"[s1,r2] [= [q1,p2] by Th21;
then [s1,r2] [= c by A14;
hence thesis by A15,Th36;
end;
set p1 = the Element of L1;
let p2,q2;
consider c being Element of [:L1,L2:] such that
A18: [p1,p2]"/\"c [= [p1,q2] and
A19: for d being Element of [:L1,L2:] st [p1,p2]"/\"d [= [p1,q2] holds d
[= c by A12;
consider r1,r2 such that
A20: c = [r1,r2] by DOMAIN_1:1;
take r2;
A21: [p1,p2]"/\"c = [p1"/\"r1,p2"/\"r2] by A20,Th21;
hence p2"/\"r2 [= q2 by A18,Th36;
let s2;
assume
A22: p2"/\"s2 [= q2;
p1"/\"r1 [= p1 by A18,A21,Th36;
then [p1"/\"r1,p2"/\"s2] [= [p1,q2] by A22,Th36;
then [p1,p2]"/\"[r1,s2] [= [p1,q2] by Th21;
then [r1,s2] [= c by A19;
hence s2 [= r2 by A20,Th36;
end;
theorem
[:L1,L2:].: = [:L1.:,L2.: :];
theorem
[:L1,L2:], [:L2,L1:] are_isomorphic
proof
set R = LattRel [:L1,L2:];
set S = LattRel [:L2,L1:];
set D1 = the carrier of L1;
set D2 = the carrier of L2;
set p2 = pr2(D1,D2);
set p1 = pr1(D1,D2);
take f = <:p2, p1:>;
A1: dom p2 = [:D1,D2:] by FUNCT_3:def 5;
A2: field R = the carrier of [:L1,L2:] by Th32;
A3: rng p2 = D2 by FUNCT_3:46;
A4: field S = the carrier of [:L2,L1:] by Th32;
dom p1 = [:D1,D2:] by FUNCT_3:def 4;
then dom p2 /\ dom p1 = [:D1,D2:] by A1;
hence
A5: dom f = field R by A2,FUNCT_3:def 7;
rng p1 = D1 by FUNCT_3:44;
hence rng f c= field S by A4,A3,FUNCT_3:51;
thus field S c= rng f
proof
let x be object;
assume x in field S;
then consider r2,r1 such that
A6: x = [r2,r1] by A4,DOMAIN_1:1;
A7: p2.(r1,r2) = r2 by FUNCT_3:def 5;
A8: p1.(r1,r2) = r1 by FUNCT_3:def 4;
f.[r1,r2] in rng f by A2,A5,FUNCT_1:def 3;
hence thesis by A2,A5,A6,A7,A8,FUNCT_3:def 7;
end;
thus f is one-to-one
proof
let x,y be object;
assume
A9: x in dom f;
then
A10: f.x = [p2.x,p1.x] by FUNCT_3:def 7;
consider r1,r2 such that
A11: x = [r1,r2] by A2,A5,A9,DOMAIN_1:1;
A12: p2.(r1,r2) = r2 by FUNCT_3:def 5;
A13: p1.(r1,r2) = r1 by FUNCT_3:def 4;
assume that
A14: y in dom f and
A15: f.x = f.y;
A16: f.y = [p2.y,p1.y] by A14,FUNCT_3:def 7;
consider q1,q2 such that
A17: y = [q1,q2] by A2,A5,A14,DOMAIN_1:1;
A18: p2.(q1,q2) = q2 by FUNCT_3:def 5;
p1.(q1,q2) = q1 by FUNCT_3:def 4;
then r1 = q1 by A11,A15,A17,A13,A10,A16,XTUPLE_0:1;
hence thesis by A11,A15,A17,A12,A18,A10,A16,XTUPLE_0:1;
end;
let x,y be object;
thus [x,y] in R implies x in field R & y in field R & [f.x,f.y] in S
proof
assume [x,y] in R;
then consider a,b being Element of [:L1,L2:] such that
A19: [x,y] = [a,b] and
A20: a [= b;
consider q1,q2 such that
A21: b = [q1,q2] by DOMAIN_1:1;
A22: f.(q1,q2) = [p2.(q1,q2),p1.(q1,q2)] by A2,A5,A21,FUNCT_3:def 7;
A23: p2.(q1,q2) = q2 by FUNCT_3:def 5;
consider r1,r2 such that
A24: a = [r1,r2] by DOMAIN_1:1;
A25: r2 [= q2 by A20,A24,A21,Th36;
r1 [= q1 by A20,A24,A21,Th36;
then
A26: [r2,r1] [= [q2,q1] by A25,Th36;
A27: p1.(r1,r2) = r1 by FUNCT_3:def 4;
A28: p2.(r1,r2) = r2 by FUNCT_3:def 5;
A29: y = b by A19,XTUPLE_0:1;
A30: x = a by A19,XTUPLE_0:1;
hence x in field R & y in field R by A2,A29;
A31: p1.(q1,q2) = q1 by FUNCT_3:def 4;
f.(r1,r2) = [p2.(r1,r2),p1.(r1,r2)] by A2,A5,A24,FUNCT_3:def 7;
hence thesis by A24,A21,A30,A29,A26,A27,A28,A31,A23,A22;
end;
assume that
A32: x in field R and
A33: y in field R;
consider q1,q2 such that
A34: y = [q1,q2] by A2,A33,DOMAIN_1:1;
A35: f.(q1,q2) = [p2.(q1,q2),p1.(q1,q2)] by A2,A5,A34,FUNCT_3:def 7;
assume
A36: [f.x,f.y] in S;
A37: p2.(q1,q2) = q2 by FUNCT_3:def 5;
A38: p1.(q1,q2) = q1 by FUNCT_3:def 4;
consider r1,r2 such that
A39: x = [r1,r2] by A2,A32,DOMAIN_1:1;
A40: p2.(r1,r2) = r2 by FUNCT_3:def 5;
A41: p1.(r1,r2) = r1 by FUNCT_3:def 4;
f.(r1,r2) = [p2.(r1,r2),p1.(r1,r2)] by A2,A5,A39,FUNCT_3:def 7;
then
A42: [r2,r1] [= [q2,q1] by A39,A34,A36,A41,A40,A35,A38,A37,Th31;
then
A43: r1 [= q1 by Th36;
r2 [= q2 by A42,Th36;
then [r1,r2] [= [q1,q2] by A43,Th36;
hence thesis by A39,A34;
end;
reserve B for B_Lattice,
a,b,c,d for Element of B;
theorem Th50:
a <=> b = (a"/\"b)"\/"(a`"/\"b`)
proof
thus a <=> b = (a`"\/"b)"/\"(b => a) by FILTER_0:42
.= (a`"\/"b)"/\"(b`"\/"a) by FILTER_0:42
.= (a`"/\"(b`"\/"a))"\/"(b"/\"(b`"\/"a)) by LATTICES:def 11
.= ((a`"/\"b`)"\/"(a`"/\"a))"\/"(b"/\"(b`"\/"a)) by LATTICES:def 11
.= ((a`"/\"b`)"\/"(a`"/\"a))"\/"((b"/\"b`)"\/"(b"/\" a)) by LATTICES:def 11
.= ((a`"/\"b`)"\/"Bottom B)"\/"((b"/\"b`)"\/"(b"/\"a)) by LATTICES:20
.= ((a`"/\"b`)"\/"Bottom B)"\/"(Bottom B"\/"(b"/\"a)) by LATTICES:20
.= (a`"/\"b`)"\/"(Bottom B"\/"(b"/\"a))
.= (a"/\"b)"\/"(a`"/\"b`);
end;
theorem Th51:
(a => b)` = a "/\" b` & (a <=> b)` = (a "/\" b`) "\/" (a` "/\" b
) & (a <=> b)` = a <=> b` & (a <=> b)` = a` <=> b
proof
A1: now
let a,b;
thus (a => b)` = (a` "\/" b)` by FILTER_0:42
.= a`` "/\" b` by LATTICES:24
.= a "/\" b`;
end;
hence (a => b)` = a "/\" b`;
thus (a <=> b)` = (a=>b)`"\/"(b=>a)` by LATTICES:23
.= (a"/\"b`)"\/"(b=>a)` by A1
.= (a"/\"b`)"\/"(a`"/\"b) by A1;
hence (a <=> b)` = (a"/\"b`)"\/"(a`"/\"b``)
.= a <=> b` by Th50;
hence (a <=> b)` = (a"/\"b`)"\/"(a`"/\"b``) by Th50
.= (a``"/\"b`)"\/"(a`"/\"b``)
.= (a`"/\"b)"\/"(a``"/\"b`)
.= a` <=> b by Th50;
end;
theorem Th52:
a <=> b = a <=> c implies b = c
proof
set ab = a"/\"b;
set ac = a"/\"c;
set bc = b"/\"c;
set b9c9 = b`"/\"c`;
set a9b9 = a`"/\"b`;
set a9c9 = a`"/\"c`;
set a9b = a`"/\"b;
set a9c = a`"/\"c;
set ab9 = a"/\"b`;
set ac9 = a"/\"c`;
A1:(a<=>b) <=> (a<=>c) = ((a<=>b)"/\"(a<=>c))"\/"((a<=>b)`"/\"(a<=>c)`)
by Th50;
A2: a<=>b = ab"\/"a9b9 & a<=>c = ac"\/"a9c9
by Th50;
A3: (a<=>b)` = ab9"\/"a9b
by Th51;
A4: (a<=>c)` = ac9"\/"a9c
by Th51;
A5: (ab"\/"a9b9)"/\"(ac"\/"a9c9) = (ab"/\"(ac"\/"a9c9))"\/"(a9b9"/\"(ac"\/"
a9c9))
by LATTICES:def 11;
A6: ab"/\"(ac"\/"a9c9) = (ab"/\"ac)"\/"(ab"/\"a9c9) & ab"/\"a9c9 = ab"/\"a`"/\"
c`
by LATTICES:def 7,def 11;
A7: a9b9"/\"(ac"\/"a9c9) = (a9b9"/\"ac)"\/"(a9b9"/\"a9c9)
by LATTICES:def 11;
A8:b"/\"a"/\"a` = b "/\"(a"/\"a`)
by LATTICES:def 7;
A9: a9b9"/\"ac = a9b9"/\"a"/\"c
by LATTICES:def 7;
A10: b`"/\"a`"/\"a = b`"/\"(a`"/\"a)
by LATTICES:def 7;
A11: (ab9"\/"a9b)"/\"(ac9"\/"a9c) = (ab9"/\"(ac9"\/"a9c))"\/"(a9b"/\"(ac9"\/"
a9c))
by LATTICES:def 11;
A12
: ab9"/\"(ac9"\/"a9c) = (ab9"/\"ac9)"\/"(ab9"/\"a9c) & ab9"/\"a9c = ab9"/\"a`
"/\"c
by LATTICES:def 7,def 11;
A13: a9b"/\"(ac9"\/"a9c) = (a9b"/\"ac9)"\/"(a9b"/\"a9c)
by LATTICES:def 11;
A14: b`"/\"a"/\"a` = b`"/\" (a"/\"a`)
by LATTICES:def 7;
A15: b"/\"Bottom B = Bottom B & Bottom B"/\"c` =
Bottom B & Bottom B"/\"c = Bottom B &
a"/\"a` = Bottom B & a`"/\"a = Bottom B & ab9 = b`"/\"a & a9b = b"/\"a` &
a9b"/\"ac9 = a9b"/\"a"/\"c` & b"/\"a`"/\"a = b"/\"(a`"/\"a) &
(ab9"/\"ac9)"\/"Bottom B = ab9"/\"ac9 & Bottom
B"\/"(a9b"/\"a9c) = a9b"/\"a9c by LATTICES:20,def 7;
ab"/\"ac = ab"/\"a"/\"c & ab"/\"a = a"/\"ab & a"/\"ab = a"/\"a"/\"b & a "/\"
a = a &
a9b9"/\"a9c9 = a9b9"/\"a`"/\"c` & a9b9"/\"a` = a`"/\"a9b9 & a`"/\"a9b9 = a`
"/\"a`"/\"b` &
a`"/\"a` = a` & ab9"/\"ac9 = ab9"/\"a"/\"c` & ab9"/\"a = a"/\"ab9 & (a"/\"b
"/\"c) = a"/\"bc &
a"/\"ab9 = a"/\"a"/\"b` & a9b"/\"a9c = a9b"/\"a`"/\"c & a9b"/\"a` = a`"/\"
a9b &
(a`"/\"b"/\"c) = a`"/\"bc & (a"/\"b`"/\"c`) = a"/\"b9c9 & (a`"/\"b`"/\"c`)
= a`"/\"b9c9 & a`"/\"a9b = a`"/\"a`"/\"b &
(a"/\"bc)"\/"(a`"/\"b9c9)"\/"((a"/\"b9c9)"\/"(a`"/\"bc)) =
(a"/\"bc)"\/"(a`"/\"b9c9)"\/"(a"/\"b9c9)"\/"(a`"/\"bc) &
(a"/\"bc)"\/"(a`"/\"b9c9)"\/"(a"/\"b9c9) = (a"/\"b9c9)"\/"((a"/\"bc)"\/"(a`
"/\"b9c9)) &
(a"/\"b9c9)"\/"((a"/\"bc)"\/"(a`"/\"b9c9)) = (a"/\"b9c9)"\/"(a"/\"bc)"\/"
(a`"/\"b9c9) &
(a"/\"b9c9)"\/"(a"/\"bc) = a"/\"(b9c9"\/"bc) & b9c9"\/"bc = bc"\/"b9c9 &
(a`"/\"b9c9)"\/"(a`"/\"bc) = a`"/\"(b9c9"\/"bc) & (Top B)"/\"(b9c9"\/"
bc) = b9c9"\/"bc & (a"/\"(b9c9"\/"bc))"\/"(a`"/\"b9c9)"\/"(a`"/\"bc) =
(a"/\"(b9c9"\/"bc))"\/"((a`"/\"b9c9)"\/"(a`"/\"bc)) & a"\/"a` = Top B &
(a"/\"(b9c9"\/"bc))"\/"(a`"/\"(b9c9"\/"bc)) = (a"\/"a`)"/\"(b9c9"\/"bc)
by LATTICES:21,def 5,def 7,def 11;
then A16: (a<=>b) <=> (a<=>c) = b <=> c by A2,A1,Th50,A3,A4,A5,A6,A7,A8,A14,
A15
,A9,A10,A11,A12,A13;
assume A17: a<=>b = a<=>c;
then
A18: (a<=>b) => (a<=>c) = Top B by FILTER_0:28;
A19: b <=> c = Top B by A16,A17,A18;
then A20: b"/\"Top B [= b"/\"(b => c) by LATTICES:6,9;
A21: c"/\"Top B [= c"/\"(c => b) by A19,LATTICES:6,9;
A22: b"/\"(b => c) [= c by FILTER_0:def 7;
A23: c"/\"(c => b) [= b by FILTER_0:def 7;
A24: b [= c by A20,A22,LATTICES:7;
c [= b by A21,A23,LATTICES:7;
hence thesis by A24,LATTICES:8;
end;
theorem Th53:
a <=> (a <=> b) = b
proof
A1: a"/\"((a"/\"b)"\/"(a`"/\"b`)) = (a"/\"(a"/\"b))"\/"(a"/\"(a`"/\"b`)) by
LATTICES:def 11;
A2: a`"/\"((a"/\"b`)"\/"(a`"/\"b)) = (a`"/\"(a"/\"b`))"\/"(a`"/\"(a`"/\"b))
by LATTICES:def 11;
A3: a"\/"a` = Top B by LATTICES:21;
A4: (a"/\"b)"\/"(a`"/\"b) = (a"\/"a`)"/\"b by LATTICES:def 11;
A5: (a<=>b)` = (a"/\"b`)"\/"(a`"/\"b) by Th51;
A6: a`"/\"(a"/\"b`) = a`"/\"a"/\"b` by LATTICES:def 7;
A7: a"/\"a` = Bottom B by LATTICES:20;
A8: a<=>b = (a"/\"b)"\/"(a`"/\"b`) by Th50;
A9: a"/\"(a"/\"b) = a"/\"a"/\"b by LATTICES:def 7;
A10: a"/\"(a`"/\"b`) = a"/\"a`"/\"b` by LATTICES:def 7;
A11: a`"/\"(a`"/\"b) = a`"/\"a`"/\"b by LATTICES:def 7;
a<=>(a<=>b) = (a"/\"(a<=>b))"\/"(a`"/\"(a<=>b)`) by Th50;
hence thesis by A8,A5,A1,A2,A9,A6,A11,A10,A7,A4,A3;
end;
theorem
(i"\/"j) => i = j => i & i => (i"/\"j) = i => j
proof
j"/\"(j=>i) [= i by FILTER_0:def 7;
then
A1: i"\/"(j"/\"(j=>i)) [= i;
A2: (i"\/"j)"/\"(j=>i) [= (i"\/"j)"/\"(i"\/" (j=>i)) by LATTICES:5,9;
A3: j"/\"((i"\/"j)=>i) [= (i"\/"j)"/\"((i"\/" j)=>i) by LATTICES:5,9;
(i"\/"j)"/\"((i"\/"j)=>i) [= i by FILTER_0:def 7;
then j"/\"((i"\/"j)=>i) [= i by A3,LATTICES:7;
then
A4: (i"\/"j)=>i [= j=>i by FILTER_0:def 7;
i"\/"(j"/\"(j=>i)) = (i"\/"j)"/\"(i"\/"(j=> i)) by LATTICES:11;
then (i"\/"j)"/\"(j=>i) [= i by A1,A2,LATTICES:7;
then j=>i [= (i"\/"j)=>i by FILTER_0:def 7;
hence (i"\/"j) => i = j => i by A4,LATTICES:8;
A5: j"/\"i [= j by LATTICES:6;
i"/\"(i=>(i"/\"j)) [= i"/\"j by FILTER_0:def 7;
then i"/\"(i=>(i"/\"j)) [= j by A5,LATTICES:7;
then
A6: i=>(i"/\"j) [= i=>j by FILTER_0:def 7;
i"/\"(i=>j) [= j by FILTER_0:def 7;
then
A7: i"/\"(i"/\"(i=>j)) [= i"/\"j by LATTICES:9;
i"/\"(i"/\"(i=>j)) = i"/\"i"/\"(i=>j) by LATTICES:def 7;
then i=>j [= i=>(i"/\"j) by A7,FILTER_0:def 7;
hence thesis by A6,LATTICES:8;
end;
theorem Th55:
i => j [= i => (j"\/"k) & i => j [= (i"/\"k) => j & i => j [= i
=> (k"\/"j) & i => j [= (k"/\"i) => j
proof
A1: i"/\"(i=>j) [= j by FILTER_0:def 7;
(i"/\"k)"/\"(i=>j) [= i"/\" (i=>j) by LATTICES:6,9;
then
A2: (i"/\"k)"/\"(i=>j) [= j by A1,LATTICES:7;
j [= j"\/"k by LATTICES:5;
then i"/\"(i=>j) [= j"\/"k by A1,LATTICES:7;
hence thesis by A2,FILTER_0:def 7;
end;
Lm1: i => j in FI implies i => (j"\/"k) in FI & i => (k"\/"j) in FI & (i"/\"k)
=> j in FI & (k"/\"i) => j in FI
proof
A1: i => j [= (i"/\"k) => j by Th55;
i => j [= i => (j"\/"k) by Th55;
hence thesis by A1,FILTER_0:9;
end;
theorem Th56:
(i => k)"/\"(j => k) [= (i"\/"j) => k
proof
A1: (i"/\"((i=>k)"/\"(j=>k)))"\/"(j"/\"((i=>k)"/\"(j=>k))) = (i"\/"j)"/\" ((
i=>k)"/\"(j=>k)) by LATTICES:def 11;
A2: j"/\"((j=>k)"/\"(i=>k)) = j"/\"(j=>k) "/\"(i=>k) by LATTICES:def 7;
j"/\"(j=>k) [= k by FILTER_0:def 7;
then
A3: j"/\"(j=>k)"/\"(i=>k) [= k by FILTER_0:2;
i"/\"(i=>k) [= k by FILTER_0:def 7;
then
A4: i"/\"(i=>k)"/\"(j=>k) [= k by FILTER_0:2;
i"/\"((i=>k)"/\"(j=>k)) = i"/\"(i=>k)"/\"(j=>k) by LATTICES:def 7;
then (i"\/"j)"/\"((i=>k)"/\"(j=>k)) [= k by A4,A3,A1,A2,FILTER_0:6;
hence thesis by FILTER_0:def 7;
end;
Lm2: i => k in FI & j => k in FI implies (i"\/"j) => k in FI
proof
assume that
A1: i => k in FI and
A2: j => k in FI;
A3: (i=>k)"/\"(j=>k) [= (i"\/"j)=> k by Th56;
(i=>k)"/\"(j=>k) in FI by A1,A2,FILTER_0:8;
hence thesis by A3,FILTER_0:9;
end;
theorem Th57:
(i => j)"/\"(i => k) [= i => (j"/\"k)
proof
A1: i"/\"(i=>j) [= j by FILTER_0:def 7;
i"/\"(i=>k) [= k by FILTER_0:def 7;
then
A2: (i"/\"(i=>j))"/\"(i"/\"(i=>k)) [= j"/\"k by A1,FILTER_0:5;
A3: (i"/\"(i=>j))"/\"(i"/\"(i=>k)) = ((i"/\"(i=>j))"/\"i)"/\"(i=>k) by
LATTICES:def 7;
A4: i"/\"((i=>j)"/\"(i=>k)) = i"/\"(i=>j)"/\" (i=>k) by LATTICES:def 7;
A5: i"/\"(i"/\"(i=>j)) = i"/\"i"/\" (i=>j) by LATTICES:def 7;
thus thesis by A2,A3,A5,A4,FILTER_0:def 7;
end;
Lm3: i => j in FI & i => k in FI implies i => (j"/\"k) in FI
proof
assume that
A1: i => j in FI and
A2: i => k in FI;
A3: (i=>j)"/\"(i=>k) [= i=>(j"/\"k) by Th57;
(i=>j)"/\"(i=>k) in FI by A1,A2,FILTER_0:8;
hence thesis by A3,FILTER_0:9;
end;
theorem Th58:
i1 <=> i2 in FI & j1 <=> j2 in FI implies (i1"\/"j1) <=> (i2"\/"
j2) in FI & (i1"/\"j1) <=> (i2"/\"j2) in FI
proof
assume that
A1: i1 <=> i2 in FI and
A2: j1 <=> j2 in FI;
A3: j1=>j2 in FI by A2,FILTER_0:8;
then
A4: (i1"/\"j1)=>j2 in FI by Lm1;
A5: j1=>(i2"\/"j2) in FI by A3,Lm1;
A6: i1=>i2 in FI by A1,FILTER_0:8;
then i1=>(i2"\/"j2) in FI by Lm1;
then
A7: (i1"\/"j1) => (i2"\/"j2) in FI by A5,Lm2;
A8: j2=>j1 in FI by A2,FILTER_0:8;
then
A9: (i2"/\"j2)=>j1 in FI by Lm1;
A10: i2=>i1 in FI by A1,FILTER_0:8;
then (i2"/\"j2)=>i1 in FI by Lm1;
then
A11: (i2"/\"j2) => (i1"/\"j1) in FI by A9,Lm3;
A12: j2=>(i1"\/"j1) in FI by A8,Lm1;
i2=>(i1"\/"j1) in FI by A10,Lm1;
then
A13: (i2"\/"j2) => (i1"\/"j1) in FI by A12,Lm2;
(i1"/\"j1)=>i2 in FI by A6,Lm1;
then (i1"/\"j1) => (i2"/\"j2) in FI by A4,Lm3;
hence thesis by A11,A7,A13,FILTER_0:8;
end;
Lm4: i in Class(equivalence_wrt FI,j) iff i <=> j in FI
proof
i in Class(equivalence_wrt FI,j) iff [i,j] in equivalence_wrt FI by
EQREL_1:19;
hence thesis by FILTER_0:def 11;
end;
theorem Th59:
i in Class(equivalence_wrt FI,k) & j in Class(equivalence_wrt FI
,k) implies i"\/"j in Class(equivalence_wrt FI,k) & i"/\" j in Class(
equivalence_wrt FI,k)
proof
assume that
A1: i in Class(equivalence_wrt FI,k) and
A2: j in Class(equivalence_wrt FI,k);
A3: i <=> k in FI by A1,Lm4;
A4: j <=> k in FI by A2,Lm4;
k"/\"k = k;
then
A5: (i"/\"j) <=> k in FI by A3,A4,Th58;
k"\/"k = k;
then (i"\/"j) <=> k in FI by A3,A4,Th58;
hence thesis by A5,Lm4;
end;
theorem Th60:
c"\/"(c <=>d) in Class(equivalence_wrt <.d.),c) & for b st b in
Class(equivalence_wrt <.d.),c) holds b [= c"\/"(c <=>d)
proof
set A = Class(equivalence_wrt <.d.),c);
A1: c in A by EQREL_1:20;
A2: (c <=>d)<=>c = c <=>(c <=>d);
A3: d in <.d.);
c <=>(c <=>d) = d by Th53;
then c <=>d in A by A3,A2,Lm4;
hence (c"\/"(c <=>d)) in A by A1,Th59;
let b;
assume b in A;
then b<=>c in <.d.) by Lm4;
then
A4: d [= b<=>c by FILTER_0:15;
(b<=>c)` = (b"/\"c`)"\/"(b`"/\"c) by Th51;
then (b"/\"c`)"\/"(b`"/\"c) [= d` by A4,LATTICES:26;
then
A5: ((b"/\"c`)"\/"(b`"/\"c))"/\"c` [= d`"/\"c` by LATTICES:9;
A6: ((b"/\"c`)"\/"(b`"/\"c))"/\"c` = ((b"/\"c`)"/\"c`)"\/"((b`"/\"c)"/\"c`)
by LATTICES:def 11;
A7: (b`"/\"c)"/\"c`= b`"/\"(c"/\"c`) by LATTICES:def 7;
A8: (c`"/\"d`)"\/"(b"/\"c) [= (c`"/\"d`)"\/"c by FILTER_0:1,LATTICES:6;
A9: (b"/\"c`)"\/"(b"/\" c) = b "/\"(c`"\/"c) by LATTICES:def 11;
A10: c"\/"(c"/\"d)"\/"(c`"/\"d`) = c"\/"((c"/\"d)"\/"(c`"/\"d`)) by
LATTICES:def 5;
A11: c = c"\/"(c"/\"d) by LATTICES:def 8;
A12: (c"/\"d)"\/"(c`"/\" d`) = c <=>d by Th50;
A13: c`"\/"c = Top B by LATTICES:21;
A14: Bottom B = c"/\"c` by LATTICES:20;
(b"/\"c`)"/\"c`= b"/\"(c `"/\" c`) by LATTICES:def 7;
then (b"/\"c`)"\/"(b"/\"c) [= (c`"/\"d`)"\/"(b"/\"c) by A5,A6,A7,A14,
FILTER_0:1;
hence thesis by A9,A13,A8,A11,A12,A10,LATTICES:7;
end;
theorem
B, [:B/\/<.a.),latt <.a.):] are_isomorphic
proof
set F = <.a.);
set E = equivalence_wrt F;
deffunc F(object) = Class(E,$1);
consider g being Function such that
A1: dom g = the carrier of B &
for x being object st x in the carrier of B holds g.x
= F(x) from FUNCT_1:sch 3;
A2: (b"\/"(b<=>a)) <=> b = b"\/"a
proof
A3: (b"\/"(b<=>a))` = b`"/\"(b<=>a)` by LATTICES:24;
A4: b`"/\"((b"/\"a`)"\/"(b`"/\"a)) = (b`"/\"(b"/\"a`))"\/"(b`"/\"(b`"/\" a
)) by LATTICES:def 11;
A5: b"\/"((b"/\"a)"\/"(b`"/\"a`)) = b"\/"(b "/\"a)"\/"(b`"/\"a`) by
LATTICES:def 5;
A6: b<=>a = (b"/\"a)"\/"(b`"/\"a`) by Th50;
A7: b`"/\"b = Bottom B by LATTICES:20;
A8: b`"/\"(a`"/\" b) = b`"/\"a`"/\"b by LATTICES:def 7;
A9: b`"/\"(b`"/\"a) = b` "/\"b`"/\"a by LATTICES:def 7;
A10: (b<=>a)` = (b"/\"a`)"\/"(b`"/\"a) by Th51;
A11: b`"/\"(b"/\"a`) = b`"/\"b"/\"a` by LATTICES:def 7;
A12: (b"\/"(b`"/\"a`))"/\"b = (b"/\"b)"\/"(b`"/\"a`"/\"b) by LATTICES:def 11;
A13: (b"/\"a)"\/"b = b by LATTICES:def 8;
(b"\/"(b<=>a)) <=> b = ((b"\/"(b<=>a))"/\"b)"\/"((b"\/"(b<=>a))` "/\"
b` ) by Th50;
hence (b"\/"(b<=>a)) <=> b = b"\/"((b"/\"a)"\/"(b`"/\" a)) by A3,A10,A4,A11
,A7,A9,A6,A5,A13,A12,A8,LATTICES:def 5
.= b"\/"((b"\/"b`)"/\"a) by LATTICES:def 11
.= b"\/"(Top B"/\"a) by LATTICES:21
.= b"\/"a;
end;
set S = LattRel [:B/\/F,latt F:];
A14: field S = the carrier of [:B/\/F,latt F:] by Th32;
reconsider o1 = join(B), o2 = meet(B) as BinOp of E by Th13,Th14;
A15: LattStr(#Class E,o1/\/E,o2/\/E#) = B/\/F by Def5;
set R = LattRel B;
deffunc F(Element of B) = ($1"\/"($1<=>a)) <=> $1;
consider h being UnOp of the carrier of B such that
A16: h.b = F(b) from FUNCT_2:sch 4;
take f = <:g,h:>;
A17: field R = the carrier of B by Th32;
A18: dom h = dom g by A1,FUNCT_2:def 1;
hence
A19: dom f = field R by A1,A17,FUNCT_3:50;
A20: h.b is Element of latt F
proof
b"\/"(b<=>a) in Class(E,b) by Th60;
then [b"\/"(b<=>a),b] in E by EQREL_1:19;
then
A21: (b"\/"(b<=>a)) <=> b in F by FILTER_0:def 11;
h.b = (b"\/"(b<=>a)) <=> b by A16;
hence thesis by A21,FILTER_0:49;
end;
thus rng f c= field S
proof
let x be object;
assume x in rng f;
then consider y being object such that
A22: y in dom f and
A23: x = f.y by FUNCT_1:def 3;
reconsider y as Element of B by A1,A18,A22,FUNCT_3:50;
reconsider z2 = h.y as Element of latt F by A20;
g.y = EqClass(E,y) by A1;
then reconsider z1 = g.y as Element of B/\/F by A15;
x = [z1,z2] by A22,A23,FUNCT_3:def 7;
hence thesis by A14;
end;
A24: the carrier of latt F = F by FILTER_0:49;
thus field S c= rng f
proof
let x be object;
assume x in field S;
then consider y being Element of Class E, z being Element of F such that
A25: x = [y,z] by A14,A24,A15,DOMAIN_1:1;
consider b such that
A26: y = Class(E,b) by EQREL_1:36;
set ty = b"\/"(b<=>a);
ty <=> (ty <=> z) = z by Th53;
then (ty <=> z) <=> ty = z;
then
A27: [ty <=> z,ty] in E by FILTER_0:def 11;
ty in y by A26,Th60;
then y = Class(E,ty) by A26,EQREL_1:23;
then
A28: ty <=> z in y by A27,EQREL_1:19;
then
A29: y = Class(E,ty<=>z) by A26,EQREL_1:23;
then
A30: ty [= (ty<=>z)"\/"((ty<=>z)<=>a ) by A26,Th60;
y = Class(E,ty<=>z) by A26,A28,EQREL_1:23;
then
A31: g.(ty <=> z) = y by A1;
(ty<=>z)"\/"((ty<=>z)<=>a) [= ty by A26,A29,Th60;
then
A32: (ty<=>z)"\/"((ty<=>z)<=>a) = ty by A30,LATTICES:8;
h.(ty<=>z) = ((ty<=>z)"\/"((ty<=>z)<=>a)) <=> (ty<=>z) by A16;
then h.(ty <=> z) = z by A32,Th53;
then x = f.(ty <=> z) by A17,A19,A25,A31,FUNCT_3:def 7;
hence thesis by A17,A19,FUNCT_1:def 3;
end;
thus f is one-to-one
proof
let x,y be object;
assume that
A33: x in dom f and
A34: y in dom f;
reconsider x9 = x, y9 = y as Element of B by A1,A18,A33,A34,FUNCT_3:50;
assume
A35: f.x = f.y;
A36: g.y9 = Class(E,y9) by A1;
A37: h.y9 = (y9"\/"(y9<=>a)) <=> y9 by A16;
A38: h.x9 = (x9"\/"(x9<=>a)) <=> x9 by A16;
A39: g.x9 = Class(E,x9) by A1;
A40: f.y = [g.y9,h.y9] by A17,A19,FUNCT_3:def 7;
A41: f.x = [g.x9,h.x9] by A17,A19,FUNCT_3:def 7;
then
A42: g.x = g.y by A40,A35,XTUPLE_0:1;
then
A43: y9"\/"(y9<=>a) [= x9"\/"(x9<=>a ) by A39,A36,Th60;
x9"\/"(x9<=>a) [= y9"\/"(y9<=>a) by A39,A36,A42,Th60;
then
A44: y9"\/"(y9<=>a) = x9"\/"(x9<=>a) by A43,LATTICES:8;
h.x = h.y by A41,A40,A35,XTUPLE_0:1;
hence thesis by A38,A37,A44,Th52;
end;
let x,y be object;
A45: the carrier of latt F = F by FILTER_0:49;
thus [x,y] in R implies x in field R & y in field R & [f.x,f.y] in S
proof
assume
A46: [x,y] in R;
then reconsider x9 = x, y9 = y as Element of B by A17,RELAT_1:15;
A47: x9 [= y9 by A46,Th31;
thus x in field R & y in field R by A46,RELAT_1:15;
A48: Top B in F by FILTER_0:11;
x9"/\"Top B = x9;
then Top B [= x9 => y9 by A47,FILTER_0:def 7;
then x9 => y9 in F by A48;
then
A49: x9/\/F [= y9/\/F by Th16;
A50: h.x9 = (x9"\/"(x9<=>a)) <=> x9 by A16;
A51: y9"\/" (y9<=>a) in Class(E,y9) by Th60;
A52: (y9"\/"(y9<=>a)) <=> y9 = y9"\/"a by A2;
A53: (x9"\/"(x9<=>a)) <=> x9 = x9"\/"a by A2;
A54: h.y9 = (y9"\/"(y9<=>a)) <=> y9 by A16;
x9"\/"(x9<=>a) in Class(E,x9) by Th60;
then reconsider hx = h.x, hy = h.y as Element of latt F by A45,A50,A54,A51
,Lm4;
A55: Class(E,x9) = g.x9 by A1;
x9"\/"a [= y9"\/"a by A47,FILTER_0:1;
then hx [= hy by A50,A54,A53,A52,FILTER_0:51;
then
A56: [x9/\/F,hx] [= [y9/\/F,hy] by A49,Th36;
A57: y9/\/F = Class(E,y9) by Def6;
A58: Class(E,y9) = g.y9 by A1;
A59: f.y9 = [g.y9,h.y9] by A17,A19,FUNCT_3:def 7;
A60: f.x9 = [g.x9,h.x9] by A17,A19,FUNCT_3:def 7;
x9/\/F = Class(E,x9) by Def6;
hence thesis by A55,A57,A58,A60,A59,A56;
end;
assume that
A61: x in field R and
A62: y in field R;
reconsider x9 = x, y9 = y as Element of B by A61,A62,Th32;
A63: h.x9 = (x9"\/"(x9<=>a)) <=> x9 by A16;
A64: f.y9 = [g.y9,h.y9] by A17,A19,FUNCT_3:def 7;
A65: y9/\/F = Class(E,y9) by Def6;
A66: Class(E,x9) = g.x9 by A1;
A67: (y9"\/"(y9<=>a)) <=> y9 = y9"\/"a by A2;
A68: (x9"\/"(x9<=>a)) <=> x9 = x9"\/"a by A2;
A69: y9"/\" x9 [= y9 by LATTICES:6;
A70: y9"\/"(y9<=>a) in Class(E,y9) by Th60;
A71: h.y9 = (y9"\/"(y9<=>a)) <=> y9 by A16;
x9"\/"(x9<=>a) in Class(E,x9) by Th60;
then reconsider hx = h.x, hy = h.y as Element of latt F by A45,A63,A71,A70
,Lm4;
assume
A72: [f.x,f.y] in S;
A73: f.x9 = [g.x9,h.x9] by A17,A19,FUNCT_3:def 7;
A74: Class(E,y9) = g.y9 by A1;
x9/\/F = Class(E,x9) by Def6;
then
A75: [x9/\/F,hx] [= [y9/\/F,hy] by A65,A66,A74,A73,A64,A72,Th31;
then x9/\/F [= y9/\/F by Th36;
then
A76: x9 => y9 in F by Th16;
x9 => y9 = x9`"\/"y9 by FILTER_0:42;
then a [= x9`"\/"y9 by A76,FILTER_0:15;
then
A77: x9"/\"a [= x9"/\"(x9`"\/"y9) by LATTICES:9;
hx [= hy by A75,Th36;
then x9"\/"a [= y9"\/"a by A63,A71,A68,A67,FILTER_0:51;
then
A78: x9"/\"(x9"\/"a) [= x9"/\"(y9"\/"a) by LATTICES:9;
A79: x9"/\"x9` = Bottom B by LATTICES:20;
x9"/\"(x9`"\/"y9) = x9"/\"x9`"\/"(x9 "/\" y9) by LATTICES:def 11;
then x9"/\"a [= y9 by A77,A79,A69,LATTICES:7;
then
A80: (x9"/\"y9)"\/"(x9"/\"a) [= y9 by A69,FILTER_0:6;
x9 [= x9 "\/"a by LATTICES:5;
then x9"/\"(x9"\/"a) = x9 by LATTICES:4;
then x9 [= (x9"/\"y9)"\/"(x9"/\"a) by A78,LATTICES:def 11;
then x9 [= y9 by A80,LATTICES:7;
hence thesis;
end;