Copyright (c) 1991 Association of Mizar Users
environ
vocabulary LATTICES, FILTER_0, RELAT_1, EQREL_1, BINOP_1, BOOLE, FUNCT_1,
LATTICE2, ZF_LANG, SUBSET_1, FUNCT_4, WELLORD1, FUNCT_3, PARTFUN1,
FILTER_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, EQREL_1, DOMAIN_1, WELLORD1, FUNCT_3, FUNCT_4, STRUCT_0,
LATTICES, FILTER_0, LATTICE2;
constructors BINOP_1, DOMAIN_1, WELLORD1, FUNCT_3, FUNCT_4, FILTER_0,
LATTICE2, MEMBERED, EQREL_1, XBOOLE_0;
clusters LATTICES, FILTER_0, LATTICE2, RELSET_1, STRUCT_0, SUBSET_1, MEMBERED,
ZFMISC_1, XBOOLE_0, PARTFUN1;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, WELLORD1, BINOP_1, FILTER_0, LATTICE2, LATTICES,
STRUCT_0, XBOOLE_0;
theorems FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, WELLORD1, DOMAIN_1, BINOP_1,
EQREL_1, RELAT_1, ZFMISC_1, LATTICES, FILTER_0, LATTICE2, STRUCT_0,
RELSET_1, WELLORD2, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, FUNCT_2, BINOP_1;
begin
deffunc carr(LattStr) = the carrier of $1;
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,
R_D 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, F_B for Filter of B,
I for I_Lattice, F_I 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 FILTER_0:11;
consider q such that
A2: q in F2 by FILTER_0:11;
p "\/" q in F1 & p "\/" q in F2 by A1,A2,FILTER_0:10;
then reconsider D = F1 /\ F2 as non empty Subset of L
by XBOOLE_0:def 3;
D is Filter of L
proof let p,q;
(p in D & q in D iff p in F1 & q in F1 & p in F2 & q in F2) &
(p "/\" q in F1 & p "/\" q in F2 iff p in F1 & q in F1 & p in F2 & q in
F2) &
(p "/\" q in F1 & p "/\" q in F2 iff p "/\" q in F1 /\ F2)
by FILTER_0:def 1,XBOOLE_0:def 3;
hence thesis;
end;
hence thesis;
end;
theorem
<.p.) = <.q.) implies p = q
proof assume <.p.) = <.q.);
then p in <.q.) & q in <.p.) by FILTER_0:19;
then p [= q & q [= p by FILTER_0:18;
hence thesis by LATTICES:26;
end;
definition let L,F1,F2;
redefine func F1 /\ F2 -> Filter of L;
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
deffunc F(Element of D) = $1;
consider f being UnOp of D such that
A1: for x being Element of D holds f.x = F(x) from LambdaD;
take f; let x,y be Element of D;
f.x = x & f.y = y by A1;
hence 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
deffunc F(Element of D,Element of D) = $1;
consider f being BinOp of D such that
A2: for x,y being Element of D holds f.(x,y) = F(x,y)
from BinOpLambda;
take f; let x1,y1, x2,y2 be Element of D;
f.(x1,x2) = x1 & f.(y1,y2) = y1 by A2;
hence thesis;
end;
end;
reserve F,G for BinOp of D,R_D;
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;
cluster Class R -> non empty;
coherence
proof consider d being Element of D;
Class(R,d) in Class R by EQREL_1:def 5;
hence thesis;
end;
end;
definition let D; let R be Equivalence_Relation of D;
let d be Element of D;
redefine func Class(R,d) -> Element of Class R;
coherence by EQREL_1:def 5;
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
deffunc F(Element of D) = Class(R,$1);
consider f being Function of D, Class R such that
A2: for x being Element of D holds f.x = F(x) from LambdaD;
now let X; assume X in Class R;
then consider x such that
A3: x in D & X = Class(R,x) by EQREL_1:def 5;
thus X <> {} by A3,EQREL_1:28;
end;
then consider g being Function such that
A4: dom g = Class R & for X st X in Class R holds g.X in X by WELLORD2:28;
A5: rng g c= D
proof let x; assume x in rng g;
then consider y such that
A6: y in dom g & x = g.y by FUNCT_1:def 5;
x in y & y c= D by A4,A6;
hence thesis;
end;
then reconsider g as Function of Class R, D by A4,FUNCT_2:def 1,RELSET_1:
11;
take uR = f*u*g; let x,y;
assume
A7: x in Class R & y in x;
then reconsider x' = x as Element of Class R;
reconsider y' = y as Element of D by A7;
g.x in rng g by A4,A7,FUNCT_1:def 5;
then g.x in D & D = dom (f*u) & Class R = dom uR by A5,FUNCT_2:def 1;
then A8: uR.x = (f*u).(g.x) & (f*u).(g.x) = f.(u.(g.x)) by A7,FUNCT_1:22;
A9: ex x1 st x1 in D & x' = Class(R,x1) by EQREL_1:def 5;
g.x' in x by A4;
then [g.x',y'] in R by A7,A9,EQREL_1:30;
then [u.(g.x'),u.y'] in R by A1,Def1;
then u.(g.x') in Class(R,u.y') & f.(u.(g.x')) = Class(R,u.(g.x')) &
f.(u.y') = Class(R,u.y') by A2,EQREL_1:27;
hence uR.x = Class(R,u.y) by A8,EQREL_1:31;
end;
uniqueness
proof let u1,u2 be UnOp of Class R such that
A10: for x,y st x in Class R & y in x holds u1.x = Class(R,u.y) and
A11: for x,y st x in Class R & y in x holds u2.x = Class(R,u.y);
now let x; assume
A12: x in Class R;
then consider y such that
A13: y in D & x = Class(R,y) by EQREL_1:def 5;
y in x by A13,EQREL_1:28;
then u1.x = Class(R,u.y) & u2.x = Class(R,u.y) by A10,A11,A12;
hence u1.x = u2.x;
end;
hence thesis by FUNCT_2:18;
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
deffunc F(Element of D) = Class(R,$1);
consider f being Function of D, Class R such that
A2: for x being Element of D holds f.x = F(x) from LambdaD;
now let X; assume X in Class R;
then consider x such that
A3: x in D & X = Class(R,x) by EQREL_1:def 5;
thus X <> {} by A3,EQREL_1:28;
end;
then consider g being Function such that
A4: dom g = Class R & for X st X in Class R holds g.X in X by WELLORD2:28;
rng g c= D
proof let x; assume x in rng g;
then consider y such that
A5: y in dom g & x = g.y by FUNCT_1:def 5;
x in y & y c= D by A4,A5;
hence thesis;
end;
then reconsider g as Function of Class R, D by A4,FUNCT_2:def 1,RELSET_1:
11;
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
A6: for x,y being Element of Class R
holds bR.(x,y) = F(x,y) from BinOpLambda;
take bR; let x,y, x1,y1;
assume
A7: x in Class R & y in Class R & x1 in x & y1 in y;
then reconsider x' = x, y' = y as Element of Class R;
reconsider x1' = x1, y1' = y1 as Element of D by A7;
A8: ex x2 st x2 in D & x' = Class(R,x2) by EQREL_1:def 5;
A9: ex y2 st y2 in D & y' = Class(R,y2) by EQREL_1:def 5;
g.x' in x & g.y' in y by A4;
then [g.x',x1'] in R & [g.y',y1'] in R by A7,A8,A9,EQREL_1:30;
then [b.(g.x',g.y'),b.(x1',y1')] in R by A1,Def2;
then b.(g.x',g.y') in Class(R,b.(x1',y1')) & bR.(x',y') = f.(b.(g.x',g.
y')) &
f.(b.(g.x',g.y')) = Class(R,b.(g.x',g.y')) &
f.(b.(x1',y1')) = Class(R,b.(x1',y1')) by A2,A6,EQREL_1:27;
hence bR.(x,y) = Class(R,b.(x1,y1)) by EQREL_1:31;
end;
uniqueness
proof let b1,b2 be BinOp of Class R such that
A10: 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
A11: 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 such that
A12: x1 in D & x = Class(R,x1) by EQREL_1:def 5;
consider y1 such that
A13: y1 in D & y = Class(R,y1) by EQREL_1:def 5;
x1 in x & y1 in y by A12,A13,EQREL_1:28;
then b1.(x,y) = Class(R,b.(x1,y1)) &
b2.(x,y) = Class(R,b.(x1,y1)) by A10,A11;
hence b1.(x,y) = b2.(x,y);
end;
hence thesis by BINOP_1:2;
end;
end;
theorem
Th3: (F /\/ R_D).(Class(R_D,a), Class(R_D,b)) = Class(R_D, F.(a,b))
proof a in Class(R_D,a) & b in Class(R_D,b) by EQREL_1:28;
hence thesis by Def4;
end;
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[Class(R(),x)]
proof let x be Element of Class R();
ex y st y in D() & x = Class(R(),y) by EQREL_1:def 5;
hence thesis by A1;
end;
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[Class(R(),x),Class(R(),y)]
proof let x1,x2 be Element of Class R();
A2: ex y1 st y1 in D() & x1 = Class(R(),y1) by EQREL_1:def 5;
ex y2 st y2 in D() & x2 = Class(R(),y2) by EQREL_1:def 5;
hence thesis by A1,A2;
end;
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[Class(R(),x),Class(R(),y),Class(R(),z)]
proof let x1,x2,x3 be Element of Class R();
A2: ex y1 st y1 in D() & x1 = Class(R(),y1) by EQREL_1:def 5;
A3: ex y2 st y2 in D() & x2 = Class(R(),y2) by EQREL_1:def 5;
ex y3 be set st y3 in D() & x3 = Class(R(),y3) by EQREL_1:def 5;
hence thesis by A1,A2,A3;
end;
theorem
Th4: F is commutative implies F/\/R_D is commutative
proof assume
A1: for a,b holds F.(a,b) = F.(b,a);
defpred P[Element of Class R_D, Element of Class R_D] means
(F/\/R_D).($1,$2) = (F/\/R_D).($2,$1);
A2: now let x1,x2 be Element of D;
thus P[Class(R_D,x1),Class(R_D,x2)]
proof
thus (F/\/R_D).(Class(R_D,x1),Class(R_D,x2))
= Class(R_D, F.(x1,x2)) by Th3
.= Class(R_D, F.(x2,x1)) by A1
.= (F/\/R_D).(Class(R_D,x2),Class(R_D,x1)) by Th3;
end;
end;
thus for c1,c2 being Element of Class R_D holds P[c1,c2]
from SchAux2(A2);
end;
theorem
Th5: F is associative implies F/\/R_D is associative
proof assume
A1: for d,a,b holds F.(d,F.(a,b)) = F.(F.(d,a),b);
defpred P[Element of Class R_D, Element of Class R_D, Element of Class R_D]
means
(F/\/R_D).($1,(F/\/R_D).($2,$3)) = (F/\/R_D).((F/\/R_D).($1,$2),$3);
A2: now let x1,x2,x3 be Element of D;
thus P[Class(R_D,x1),Class(R_D,x2),Class(R_D,x3)]
proof
thus (F/\/R_D).(Class(R_D,x1),(F/\/R_D).(Class(R_D,x2),Class(R_D,x3)))
= (F/\/R_D).(Class(R_D,x1),Class(R_D, F.(x2,x3))) by Th3
.= Class(R_D, F.(x1,F.(x2,x3))) by Th3
.= Class(R_D, F.(F.(x1,x2),x3)) by A1
.= (F/\/R_D).(Class(R_D,F.(x1,x2)),Class(R_D, x3)) by Th3
.= (F/\/R_D).((F/\/R_D).(Class(R_D,x1),Class(R_D,x2)),Class(R_D,x3))
by Th3;
end;
end;
thus for c1,c2,c3 being Element of Class R_D holds P[c1,c2,c3]
from SchAux3(A2);
end;
theorem
Th6: d is_a_left_unity_wrt F implies Class(R_D,d) is_a_left_unity_wrt F/\/R_D
proof assume
A1: F.(d,a) = a;
defpred P[Element of Class R_D] means
(F/\/R_D).(Class(R_D,d),$1) = $1;
A2: now let a;
thus P[Class(R_D,a)]
proof
thus (F/\/R_D).(Class(R_D,d),Class(R_D,a))
= Class(R_D, F.(d,a)) by Th3 .= Class(R_D, a) by A1;
end;
end;
thus for c being Element of Class R_D holds P[c]
from SchAux1(A2);
end;
theorem
Th7: d is_a_right_unity_wrt F implies
Class(R_D,d) is_a_right_unity_wrt F/\/R_D
proof assume
A1: F.(a,d) = a;
defpred P[Element of Class R_D] means
(F/\/R_D).($1,Class(R_D,d)) = $1;
A2: now let a;
thus P[Class(R_D,a)]
proof
thus (F/\/R_D).(Class(R_D,a),Class(R_D,d))
= Class(R_D, F.(a,d)) by Th3 .= Class(R_D, a) by A1;
end;
end;
thus for c being Element of Class R_D holds P[c]
from SchAux1(A2);
end;
theorem
d is_a_unity_wrt F implies Class(R_D,d) is_a_unity_wrt F/\/R_D
proof assume
d is_a_left_unity_wrt F & d is_a_right_unity_wrt F;
hence Class(R_D,d) is_a_left_unity_wrt F/\/R_D &
Class(R_D,d) is_a_right_unity_wrt F/\/R_D by Th6,Th7;
end;
theorem Th9:
F is_left_distributive_wrt G implies F/\/R_D is_left_distributive_wrt G/\/R_D
proof assume
A1: for d,a,b holds F.(d,G.(a,b)) = G.(F.(d,a),F.(d,b));
deffunc Cl(Element of D) = Class(R_D,$1);
defpred P[Element of Class R_D, Element of Class R_D, Element of Class R_D]
means (F/\/R_D).($1,(G/\/R_D).($2,$3)) =
(G/\/R_D).((F/\/R_D).($1,$2),(F/\/R_D).($1,$3));
A2: now let x1,x2,x3 be Element of D;
thus P[Class(R_D,x1),Class(R_D,x2),Class(R_D,x3)]
proof
thus (F/\/R_D).(Cl(x1),(G/\/R_D).(Cl(x2),Cl(x3)))
= (F/\/R_D).(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/\/R_D).(Cl(F.(x1,x2)),Cl(F.(x1,x3))) by Th3
.= (G/\/R_D).((F/\/R_D).(Cl(x1),Cl(x2)),Cl(F.(x1,x3))) by Th3
.= (G/\/R_D).((F/\/R_D).(Cl(x1),Cl(x2)),(F/\/R_D).(Cl(x1),Cl(x3)))
by Th3;
end;
end;
thus for c1,c2,c3 being Element of Class R_D holds P[c1,c2,c3]
from SchAux3(A2);
end;
theorem Th10:
F is_right_distributive_wrt G implies
F/\/R_D is_right_distributive_wrt G/\/R_D
proof assume
A1: for a,b,d holds F.(G.(a,b),d) = G.(F.(a,d),F.(b,d));
deffunc Cl(Element of D) = Class(R_D,$1);
defpred P[Element of Class R_D, Element of Class R_D, Element of Class R_D]
means (F/\/R_D).((G/\/R_D).($1,$2),$3) =
(G/\/R_D).((F/\/R_D).($1,$3),(F/\/R_D).($2,$3));
A2: now let x2,x3,x1 be Element of D;
thus P[Class(R_D,x2),Class(R_D,x3),Class(R_D,x1)]
proof
thus (F/\/R_D).((G/\/R_D).(Cl(x2),Cl(x3)),Cl(x1))
= (F/\/R_D).(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/\/R_D).(Cl(F.(x2,x1)),Cl(F.(x3,x1))) by Th3
.= (G/\/R_D).((F/\/R_D).(Cl(x2),Cl(x1)),Cl(F.(x3,x1))) by Th3
.= (G/\/R_D).((F/\/R_D).(Cl(x2),Cl(x1)),(F/\/R_D).(Cl(x3),Cl(x1)))
by Th3;
end;
end;
thus for c2,c3,c1 being Element of Class R_D holds P[c2,c3,c1]
from SchAux3(A2);
end;
theorem
F is_distributive_wrt G implies F/\/R_D is_distributive_wrt G/\/R_D
proof assume
F is_left_distributive_wrt G & F is_right_distributive_wrt G;
hence F/\/R_D is_left_distributive_wrt G/\/R_D &
F/\/R_D is_right_distributive_wrt G/\/R_D by Th9,Th10;
end;
theorem
Th12: F absorbs G implies F/\/R_D absorbs G/\/R_D
proof assume
A1: for x,y being Element of D holds F.(x,G.(x,y)) = x;
deffunc Cl(Element of D) = Class(R_D,$1);
defpred P[Element of Class R_D,Element of Class R_D] means
(F/\/R_D).($1,(G/\/R_D).($1,$2)) = $1;
A2: now let x1,x2 be Element of D;
thus P[Class(R_D ,x1),Class(R_D,x2)]
proof
thus (F/\/R_D).(Cl(x1),(G/\/R_D).(Cl(x1),Cl(x2)))
= (F/\/R_D).(Cl(x1),Cl(G.(x1,x2))) by Th3
.= Cl(F.(x1,G.(x1,x2))) by Th3
.= Cl(x1) by A1;
end;
end;
thus for x,y being Element of Class R_D holds P[x,y] from SchAux2(A2);
end;
theorem
Th13: the L_join of I is BinOp of the carrier of I, equivalence_wrt F_I
proof
set R = equivalence_wrt F_I;
set o = the L_join of I;
let x1,y1, x2,y2 be Element of (the carrier of I);
assume [x1,y1] in R & [x2,y2] in R;
then x1 <=> y1 in F_I & x2 <=> y2 in F_I &
x1 <=> y1 = (x1 => y1) "/\" (y1 => x1) &
x2 <=> y2 = (x2 => y2) "/\" (y2 => x2)
by FILTER_0:def 11,def 12;
then A1: x1 => y1 in F_I & x2 => y2 in F_I & y1 => x1 in F_I & y2 => x2 in F_I
by FILTER_0:def 1;
x2 "/\" (x1 => y1) = (x1 => y1) "/\" x2 &
(x1 => y1) "/\" (x2 "/\" (x2 => y2)) = (x1 => y1) "/\" x2 "/\" (x2 => y2) &
x1 "/\" ((x1 => y1) "/\" (x2 => y2)) = x1 "/\" (x1 => y1) "/\" (x2 => y2) &
x2 "/\" ((x1 => y1) "/\" (x2 => y2)) = x2 "/\" (x1 => y1) "/\" (x2 => y2) &
x1 "/\" (x1 => y1) [= y1 & x2 "/\" (x2 => y2) [= y2
by FILTER_0:def 8,LATTICES:def 7;
then x1 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 &
x2 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y2 by FILTER_0:2;
then x1 "/\" ((x1 => y1) "/\" (x2 => y2)) "\/" (x2 "/\" ((x1 => y1) "/\"
(x2 => y2))) [=
y1 "\/" y2 by FILTER_0:4;
then (x1 "\/" x2) "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 "\/"
y2 by LATTICES:def 11;
then (x1 => y1) "/\" (x2 => y2) [= (x1 "\/" x2) => (y1 "\/" y2) &
(x1 => y1) "/\" (x2 => y2) in F_I by A1,FILTER_0:def 1,def 8;
then A2: (x1 "\/" x2) => (y1 "\/" y2) in F_I by FILTER_0:9;
y2 "/\" (y1 => x1) = (y1 => x1) "/\" y2 &
(y1 => x1) "/\" (y2 "/\" (y2 => x2)) = (y1 => x1) "/\" y2 "/\" (y2 => x2) &
y1 "/\" ((y1 => x1) "/\" (y2 => x2)) = y1 "/\" (y1 => x1) "/\" (y2 => x2) &
y2 "/\" ((y1 => x1) "/\" (y2 => x2)) = y2 "/\" (y1 => x1) "/\" (y2 => x2) &
y1 "/\" (y1 => x1) [= x1 & y2 "/\" (y2 => x2) [= x2
by FILTER_0:def 8,LATTICES:def 7;
then y1 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 &
y2 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x2 by FILTER_0:2;
then y1 "/\" ((y1 => x1) "/\" (y2 => x2)) "\/" (y2 "/\" ((y1 => x1) "/\"
(y2 => x2))) [=
x1 "\/" x2 by FILTER_0:4;
then (y1 "\/" y2) "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 "\/"
x2 by LATTICES:def 11;
then (y1 => x1) "/\" (y2 => x2) [= (y1 "\/" y2) => (x1 "\/" x2) &
(y1 => x1) "/\" (y2 => x2) in F_I by A1,FILTER_0:def 1,def 8;
then ((x1 "\/" x2) => (y1 "\/" y2)) "/\" ((y1 "\/" y2) => (x1 "\/" x2)) =
(x1 "\/" x2) <=> (y1 "\/" y2) &
(y1 "\/" y2) => (x1 "\/" x2) in F_I by FILTER_0:9,def 11;
then (x1 "\/" x2) <=> (y1 "\/" y2) in F_I &
o.(x1,x2) = x1 "\/" x2 & o.(y1,y2) = y1 "\/" y2
by A2,FILTER_0:def 1,LATTICES:def 1;
hence [o.(x1,x2),o.(y1,y2)] in R by FILTER_0:def 12;
end;
theorem
Th14: the L_meet of I is BinOp of the carrier of I, equivalence_wrt F_I
proof
set R = equivalence_wrt F_I;
set o = the L_meet of I;
let x1,y1, x2,y2 be Element of I;
assume [x1,y1] in R & [x2,y2] in R;
then x1 <=> y1 in F_I & x2 <=> y2 in F_I &
x1 <=> y1 = (x1 => y1) "/\" (y1 => x1) &
x2 <=> y2 = (x2 => y2) "/\" (y2 => x2)
by FILTER_0:def 11,def 12;
then A1: x1 => y1 in F_I & x2 => y2 in F_I & y1 => x1 in F_I & y2 => x2 in F_I
by FILTER_0:def 1;
x1 "/\" (x1 => y1) [= y1 & x2 "/\" (x2 => y2) [= y2
by FILTER_0:def 8;
then x1 "/\" (x1 => y1) "/\" (x2 "/\" (x2 => y2)) =
x1 "/\" (x1 => y1) "/\" x2 "/\" (x2 => y2) & x2 "/\" x1 = x1 "/\" x2 &
x1 "/\" (x1 => y1) "/\" x2 = x2 "/\" (x1 "/\" (x1 => y1)) &
x2 "/\" x1 "/\" (x1 => y1) = x2 "/\" (x1 "/\" (x1 => y1)) &
x1 "/\" x2 "/\" (x1 => y1) "/\" (x2 => y2) =
x1 "/\" x2 "/\" ((x1 => y1) "/\" (x2 => y2)) &
x1 "/\" (x1 => y1) "/\" (x2 "/\" (x2 => y2)) [= y1 "/\" y2
by FILTER_0:5,LATTICES:def 7;
then (x1 => y1) "/\" (x2 => y2) [= (x1 "/\" x2) => (y1 "/\" y2) &
(x1 => y1) "/\" (x2 => y2) in F_I by A1,FILTER_0:def 1,def 8;
then A2: (x1 "/\" x2) => (y1 "/\" y2) in F_I by FILTER_0:9;
y1 "/\" (y1 => x1) [= x1 & y2 "/\" (y2 => x2) [= x2
by FILTER_0:def 8;
then y1 "/\" (y1 => x1) "/\" (y2 "/\" (y2 => x2)) =
y1 "/\" (y1 => x1) "/\" y2 "/\" (y2 => x2) & y2 "/\" y1 = y1 "/\" y2 &
y1 "/\" (y1 => x1) "/\" y2 = y2 "/\" (y1 "/\" (y1 => x1)) &
y2 "/\" y1 "/\" (y1 => x1) = y2 "/\" (y1 "/\" (y1 => x1)) &
y1 "/\" y2 "/\" (y1 => x1) "/\" (y2 => x2) =
y1 "/\" y2 "/\" ((y1 => x1) "/\" (y2 => x2)) &
y1 "/\" (y1 => x1) "/\" (y2 "/\" (y2 => x2)) [= x1 "/\" x2
by FILTER_0:5,LATTICES:def 7;
then (y1 => x1) "/\" (y2 => x2) [= (y1 "/\" y2) => (x1 "/\" x2) &
(y1 => x1) "/\" (y2 => x2) in F_I by A1,FILTER_0:def 1,def 8;
then ((x1 "/\" x2) => (y1 "/\" y2)) "/\" ((y1 "/\" y2) => (x1 "/\" x2)) =
(x1 "/\" x2) <=> (y1 "/\" y2) &
(y1 "/\" y2) => (x1 "/\" x2) in F_I by FILTER_0:9,def 11;
then (x1 "/\" x2) <=> (y1 "/\" y2) in F_I &
o.(x1,x2) = x1 "/\" x2 & o.(y1,y2) = y1 "/\" y2
by A2,FILTER_0:def 1,LATTICES:def 2;
hence [o.(x1,x2),o.(y1,y2)] in R by FILTER_0:def 12;
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 F_I = F as Filter of I;
reconsider j = the L_join of I, m = the L_meet of I as
BinOp of equivalence_wrt F_I by Th13,Th14;
reconsider LL = LattStr (#Class equivalence_wrt F_I,
j/\/equivalence_wrt F_I,
m/\/equivalence_wrt F_I#)
as non empty strict LattStr by STRUCT_0:def 1;
join(L) is commutative & join(L) is associative &
meet(L) is commutative & meet(L) is associative &
join(L) absorbs meet(L) & meet(L) absorbs join(L)
by LATTICE2:40,41;
then join(LL) is commutative & join(LL) is associative &
meet(LL) is commutative & meet(LL) is associative &
join(LL) absorbs meet(LL) & meet(LL) absorbs join(LL)
by Th4,Th5,Th12;
then reconsider LL as strict Lattice by LATTICE2:17;
take LL; thus thesis;
end;
uniqueness
proof let L1, L2 be strict Lattice such that
A2: 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
A3: 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#);
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;
thus L1 = LattStr (#Class R, o1/\/R, o2/\/R#) by A2 .= L2 by A3;
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 F_I = F as Filter of I;
reconsider i = a as Element of I;
set R = equivalence_wrt F_I;
reconsider j = join(I), m = meet(I) as BinOp of R by Th13,Th14;
I /\/ F_I = LattStr (#Class R, j/\/R, m/\/R#) by Def5;
then reconsider c = Class(equivalence_wrt F_I,i)
as Element of L/\/F;
take c; thus thesis;
end;
uniqueness
proof 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 I = L as I_Lattice by A1;
reconsider F_I = F as Filter of I;
c1 = Class(equivalence_wrt F_I, a) by A2;
hence thesis by A3;
end;
end;
theorem
Th15: (i/\/F_I) "\/" (j/\/F_I) = (i"\/"j)/\/F_I &
(i/\/F_I) "/\" (j/\/F_I) = (i"/\"j)/\/F_I
proof set R = equivalence_wrt F_I;
reconsider jj = join(I), mm = meet(I) as BinOp of R by Th13,Th14;
A1: i/\/F_I = Class(R,i) & j/\/F_I = Class(R,j) &
(i"\/"j)/\/F_I = Class(R,i"\/"j) &
(i"/\"j)/\/F_I = Class(R,i"/\"j) by Def6;
A2: I /\/ F_I = LattStr (#Class R, jj/\/R, mm/\/R#) by Def5;
hence (i/\/F_I) "\/" (j/\/F_I) =
(jj/\/R).(i/\/F_I,j/\/F_I) by LATTICES:def 1
.= Class(R,jj.(i,j)) by A1,Th3 .= (i"\/"j)/\/F_I by A1,LATTICES:def 1;
thus (i/\/F_I) "/\" (j/\/F_I) =
(mm/\/R).(i/\/F_I,j/\/F_I) by A2,LATTICES:def 2
.= Class(R,mm.(i,j)) by A1,Th3 .= (i"/\"j)/\/F_I by A1,LATTICES:def 2;
end;
theorem
Th16: i/\/F_I [= j/\/F_I iff i => j in F_I
proof set R = equivalence_wrt F_I;
set a = i"\/"j; set b = a => j;
thus i/\/F_I [= j/\/F_I implies i => j in F_I
proof assume (i/\/F_I) "\/" (j/\/F_I) = j/\/F_I;
then (i"\/"j)/\/F_I = j/\/F_I & Class(R,i"\/"j) = (i"\/"j)/\/F_I &
j/\/F_I = Class(R,j) & i"\/"j in Class(R,i"\/"j) & j in Class(R,j)
by Def6,Th15,EQREL_1:28;
then [i"\/"j,j] in R & a"/\"b = (i"/\"b)"\/"(j"/\"b) & a"/\"b [= j &
i"/\"b [= (i"/\"b)"\/"(j"/\"b)
by EQREL_1:30,FILTER_0:def 8,LATTICES:22,def 11;
then (i"\/"j) <=> j in F_I & (i"\/"j) <=> j = ((i"\/"j) => j)"/\"(j =>
(i"\/"
j)) &
i"/\"b [= j by FILTER_0:def 11,def 12,LATTICES:25;
then (i"\/"j) => j in F_I & (i"\/"j) => j [= i => j by FILTER_0:def 1,
def 8;
hence thesis by FILTER_0:9;
end;
assume
A1: i => j in F_I;
i"/\"(i => j) [= j & j"/\"(i => j) [= j & j"\/"j = j &
(i"/\"(i => j))"\/"(j"/\"(i => j)) = (i"\/"j)"/\"(i => j) & j [= i"\/"j & j
"/\"Top I [= j
by FILTER_0:2,3,def 8,LATTICES:17,def 11;
then (i"\/"j)"/\"(i => j) [= j & j"/\"Top I [= i"\/"j & I is 1_Lattice
by FILTER_0:4,37,LATTICES:25;
then i => j [= (i"\/"j) => j & Top I [= j => (i"\/"j) & Top I in F_I
by FILTER_0:12,def 8;
then (i"\/"j) => j in F_I & j => (i"\/"j) in F_I &
((i"\/"j) => j)"/\"(j => (i"\/"j)) = (i"\/"j) <=> j
by A1,FILTER_0:9,def 11;
then (i"\/"j) <=> j in F_I by FILTER_0:def 1;
then A2: [i"\/"j,j] in R by FILTER_0:def 12;
thus (i/\/F_I) "\/" (j/\/F_I) = (i"\/"j)/\/F_I by Th15
.= Class(R,i"\/"j) by Def6 .= Class(R,j) by A2,EQREL_1:44
.= j/\/F_I by Def6;
end;
theorem
Th17: (i"/\"j) => k = i => (j => k)
proof
(i"/\"j)"/\"((i"/\"j)=>k) [= k & (j"/\"i)"/\"((i"/\"j)=>k) = j"/\"(i"/\"(
(
i
"/\"j)=>k)) &
i"/\"j = j"/\"i by FILTER_0:def 8,LATTICES:def 7;
then i"/\"((i"/\"j)=>k) [= j=>k by FILTER_0:def 8;
then A1: (i"/\"j)=>k [= i=>(j=>k) by FILTER_0:def 8;
i"/\"(i=>(j=>k)) [= j=>k by FILTER_0:def 8;
then j"/\"(i"/\"(i=>(j=>k))) [= j"/\"(j=>k) & j"/\"(j=>k) [= k & j"/\"i =
i"/\"
j &
j"/\"(i"/\"(i=>(j=>k))) = j"/\"i"/\"(i=>(j=>k))
by FILTER_0:def 8,LATTICES:27,def 7;
then i"/\"j"/\"(i=>(j=>k)) [= k by LATTICES:25;
then i=>(j=>k) [= (i"/\"j)=>k by FILTER_0:def 8;
hence thesis by A1,LATTICES:26;
end;
theorem
Th18: I is lower-bounded
implies I/\/F_I is 0_Lattice & Bottom (I/\/F_I) = (Bottom I)/\/F_I
proof
assume A1: I is lower-bounded;
then consider i such that
A2: i"/\"j = i & j"/\"i = i by LATTICES:def 13;
A3: Bottom I = i by A1,A2,LATTICES:def 16;
set L = I/\/F_I; set R = equivalence_wrt F_I;
set x = i/\/F_I;
A4: 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
A5: y = Class(R,j) by EQREL_1:45;
A6: i"/\"j = i & y = j/\/F_I by A2,A5,Def6;
hence x"/\"y = x by Th15;
thus y"/\"x = x by A6,Th15;
end;
hence I/\/F_I is 0_Lattice by LATTICES:def 13;
hence thesis by A3,A4,LATTICES:def 16;
end;
theorem
Th19: I/\/F_I is 1_Lattice & Top (I/\/F_I) = (Top I)/\/F_I
proof
set L = I/\/F_I; set R = equivalence_wrt F_I;
set x = (Top I)/\/F_I;
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:45;
I is 1_Lattice by FILTER_0:37;
then A3: (Top I)"\/"j = Top I & y = j/\/F_I by A2,Def6,LATTICES:44;
hence x"\/"y = x by Th15;
thus y"\/"x = x by A3,Th15;
end;
hence I/\/F_I is 1_Lattice by LATTICES:def 14;
hence thesis by A1,LATTICES:def 17;
end;
theorem
Th20: I/\/F_I is implicative
proof set L = I/\/F_I; set R = equivalence_wrt F_I;
let x,y be Element of L;
A1: L = LattStr (#Class R, (the L_join of I)/\/R, (the L_meet of I)/\/R#)
by Def5;
then consider i such that
A2: x = Class(R,i) by EQREL_1:45;
consider j such that
A3: y = Class(R,j) by A1,EQREL_1:45;
take z = (i=>j)/\/F_I;
A4: I is 1_Lattice & x = i/\/F_I & y = j/\/F_I by A2,A3,Def6,FILTER_0:37;
then i"/\"(i=>j) [= j & (i"/\"(i=>j))"/\"Top I = i"/\"(i=>j)
by FILTER_0:def 8,LATTICES:43;
then Top I [= (i"/\"(i=>j))=>j & Top I in F_I by A4,FILTER_0:12,def 8;
then (i"/\"(i=>j))=>j in F_I by FILTER_0:9;
then (i"/\"(i=>j))/\/F_I [= y by A4,Th16;
hence x"/\"z [= y by A4,Th15;
let t be Element of L;
consider k such that
A5: t = Class(R,k) by A1,EQREL_1:45;
A6: (i/\/F_I)"/\"(k/\/F_I) = (i"/\"k)/\/F_I & k/\/F_I = t by A5,Def6,Th15;
assume x"/\"t [= y;
then (i"/\"k)=>j in F_I & i"/\"k = k"/\"i by A4,A6,Th16;
then k=>(i=>j) in F_I by Th17;
hence thesis by A6,Th16;
end;
theorem
B/\/F_B is B_Lattice
proof set L = B/\/F_B; set R = equivalence_wrt F_B;
A1: B is I_Lattice & B is 0_Lattice by FILTER_0:40;
then A2: L is 0_Lattice & Bottom L = (Bottom
B)/\/F_B & L is 1_Lattice & Top L = (Top B)/\/F_B
by Th18,Th19;
then reconsider L as 01_Lattice by LATTICES:def 15;
A3: 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 A1,Def5;
then consider a being Element of B such that
A4: x = Class(R,a) by EQREL_1:45;
reconsider y = a`/\/F_B as Element of L;
take y;
A5: x = a/\/F_B by A1,A4,Def6;
hence y"\/"x = (a`"\/"a)/\/F_B by A1,Th15 .= Top L by A2,LATTICES:48;
hence x"\/"y = Top L;
thus y"/\"x = (a`"/\"a)/\/F_B by A1,A5,Th15 .= Bottom
L by A2,LATTICES:47;
hence x"/\"y = Bottom L;
end;
L is I_Lattice by A1,Th20;
hence thesis by A3,LATTICES:def 20;
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:];
coherence
proof
(D1 = {} implies [:D1,D1:] = {}) &
(D2 = {} implies [:D2,D2:] = {}) by ZFMISC_1:113;
then dom f1 = [:D1,D1:] & rng f1 c= D1 & dom f2 = [:D2,D2:] & rng f2 c=
D2
by FUNCT_2:def 1,RELSET_1:12;
then A1: [:rng f1,rng f2:] c= [:D1,D2:] & rng |:f1,f2:| c= [:rng f1,rng f2:]
&
dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:]
by FUNCT_4:59,61,ZFMISC_1:119;
then rng |:f1,f2:| c= [:D1,D2:] by XBOOLE_1:1;
hence thesis by A1,FUNCT_2:4;
end;
end;
theorem
Th22: |:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)]
proof
[[a1,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:] &
f1.(a1,b1) = f1.[a1,b1] & f2.(a2,b2) = f2.[a2,b2] &
|:f1,f2:|.([a1,a2],[b1,b2]) = |:f1,f2:|.[[a1,a2],[b1,b2]] &
dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by BINOP_1:def 1,FUNCT_2:def 1;
hence thesis by FUNCT_4:58;
end;
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:9;
hence thesis by A1;
end;
AuxCart2 { D1() -> non empty set, D2() -> non empty set, P[set,set] }:
for d,d' being Element of [:D1(),D2():] holds P[d,d']
provided
A1: for d1,d1' being Element of D1(),
d2,d2' being Element of D2() holds
P[[d1,d2],[d1',d2']]
proof let d,d' be Element of [:D1(),D2():];
A2: ex d1 being Element of D1(),
d2 being Element of D2() st
d = [d1,d2] by DOMAIN_1:9;
ex d1' being Element of D1(),
d2' being Element of D2() st
d' = [d1',d2'] by DOMAIN_1:9;
hence thesis by A1,A2;
end;
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 a1 being Element of D1(),
a2 being Element of D2() st
a = [a1,a2] by DOMAIN_1:9;
A3: ex b1 being Element of D1(),
b2 being Element of D2() st
b = [b1,b2] by DOMAIN_1:9;
ex c1 being Element of D1(),
c2 being Element of D2() st
c = [c1,c2] by DOMAIN_1:9;
hence thesis by A1,A2,A3;
end;
theorem
Th23: 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,d1' being Element of D1,
d2,d2' being Element of D2 holds
P[[d1,d2],[d1',d2']]
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 Th22
.= [f1.(b1,a1),f2.(a2,b2)] by A1
.= [f1.(b1,a1),f2.(b2,a2)] by A2
.= |:f1,f2:|.([b1,b2],[a1,a2]) by Th22;
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 let a1,b1; consider a2,b2;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th22
.= |:f1,f2:|.([b1,b2],[a1,a2]) by A4
.= [f1.(b1,a1),f2.(b2,a2)] by Th22;
hence thesis by ZFMISC_1:33;
end;
let a2,b2; consider a1,b1;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th22
.= |:f1,f2:|.([b1,b2],[a1,a2]) by A4
.= [f1.(b1,a1),f2.(b2,a2)] by Th22;
hence thesis by ZFMISC_1:33;
end;
theorem
Th24: 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 assume
A1: for a,b,c being Element of D1
holds f1.(a,f1.(b,c)) = f1.(f1.(a,b),c);
defpred P[set,set,set] means
|:f1,f2:|.($1,|:f1,f2:|.($2,$3)) = |:f1,f2:|.(|:f1,f2:|.($1,$2),$3);
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 Th22
.= [f1.(a1,f1.(b1,c1)),f2.(a2,f2.(b2,c2))] by Th22
.= [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 Th22
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[c1,c2]) by Th22;
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 let a1,b1,c1; consider a2,b2,c2;
[f1.(a1,f1.(b1,c1)), f2.(a2,f2.(b2,c2))]
= |:f1,f2:|.([a1,a2],[f1.(b1,c1),f2.(b2,c2)]) by Th22
.= |:f1,f2:|.([a1,a2],|:f1,f2:|.([b1,b2],[c1,c2])) by Th22
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[c1,c2]) by A4
.= |:f1,f2:|.([f1.(a1,b1),f2.(a2,b2)],[c1,c2]) by Th22
.= [f1.(f1.(a1,b1),c1), f2.(f2.(a2,b2),c2)] by Th22;
hence thesis by ZFMISC_1:33;
end;
let a2,b2,c2; consider a1,b1,c1;
[f1.(a1,f1.(b1,c1)), f2.(a2,f2.(b2,c2))]
= |:f1,f2:|.([a1,a2],[f1.(b1,c1),f2.(b2,c2)]) by Th22
.= |:f1,f2:|.([a1,a2],|:f1,f2:|.([b1,b2],[c1,c2])) by Th22
.= |:f1,f2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[c1,c2]) by A4
.= |:f1,f2:|.([f1.(a1,b1),f2.(a2,b2)],[c1,c2]) by Th22
.= [f1.(f1.(a1,b1),c1), f2.(f2.(a2,b2),c2)] by Th22;
hence thesis by ZFMISC_1:33;
end;
theorem
Th25: 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 assume
A1: f1.(a1,b1) = b1; assume
A2: f2.(a2,b2) = b2;
defpred P[set] means |:f1,f2:|.([a1,a2],$1) = $1;
A3: now let b1,b2;
|:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)] by Th22
.= [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 consider b2;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th22
.= [b1,b2] by A4;
hence thesis by ZFMISC_1:33;
end;
let b2; consider b1;
[f1.(a1,b1),f2.(a2,b2)] = |:f1,f2:|.([a1,a2],[b1,b2]) by Th22
.= [b1,b2] by A4;
hence thesis by ZFMISC_1:33;
end;
theorem
Th26: 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 assume
A1: f1.(b1,a1) = b1; assume
A2: f2.(b2,a2) = b2;
defpred P[set] means |:f1,f2:|.($1,[a1,a2]) = $1;
A3: now let b1,b2;
|:f1,f2:|.([b1,b2],[a1,a2]) = [f1.(b1,a1),f2.(b2,a2)] by Th22
.= [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 consider b2;
[f1.(b1,a1),f2.(b2,a2)] = |:f1,f2:|.([b1,b2],[a1,a2]) by Th22
.= [b1,b2] by A4;
hence thesis by ZFMISC_1:33;
end;
let b2; consider b1;
[f1.(b1,a1),f2.(b2,a2)] = |:f1,f2:|.([b1,b2],[a1,a2]) by Th22
.= [b1,b2] by A4;
hence thesis by ZFMISC_1:33;
end;
theorem
a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 iff
[a1,a2] is_a_unity_wrt |:f1,f2:|
proof
thus a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 implies
[a1,a2] is_a_unity_wrt |:f1,f2:|
proof assume
a1 is_a_left_unity_wrt f1 & a1 is_a_right_unity_wrt f1 &
a2 is_a_left_unity_wrt f2 & a2 is_a_right_unity_wrt f2;
hence [a1,a2] is_a_left_unity_wrt |:f1,f2:| &
[a1,a2] is_a_right_unity_wrt |:f1,f2:| by Th25,Th26;
end;
assume [a1,a2] is_a_left_unity_wrt |:f1,f2:| &
[a1,a2] is_a_right_unity_wrt |:f1,f2:|;
hence a1 is_a_left_unity_wrt f1 & a1 is_a_right_unity_wrt f1 &
a2 is_a_left_unity_wrt f2 & a2 is_a_right_unity_wrt f2 by Th25,Th26;
end;
theorem
Th28: 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 assume
A1: for a1,b1,c1 holds f1.(a1,g1.(b1,c1)) = g1.(f1.(a1,b1),f1.(a1,c1));
defpred P[set,set,set] means
|:f1,f2:|.($1,|:g1,g2:|.($2,$3)) =
|:g1,g2:|.(|:f1,f2:|.($1,$2),|:f1,f2:|.($1,$3));
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 Th22
.= [f1.(a1,g1.(b1,c1)),f2.(a2,g2.(b2,c2))] by Th22
.= [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 Th22
.= |:g1,g2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),[f1.(a1,c1),f2.(a2,c2)])
by Th22
.= |:g1,g2:|.(|:f1,f2:|.([a1,a2],[b1,b2]),|:f1,f2:|.([a1,a2],[c1,c2]))
by Th22;
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 Th22
.= |:f1,f2:|.([a1,a2],|:g1,g2:|.([b1,b2],[c1,c2])) by Th22
.= |: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 Th22
.= |:g1,g2:|.([f1.(a1,b1),f2.(a2,b2)],[f1.(a1,c1),f2.(a2,c2)]) by Th22
.= [g1.(f1.(a1,b1),f1.(a1,c1)),g2.(f2.(a2,b2),f2.(a2,c2))] by Th22;
end;
thus for a1,b1,c1 holds f1.(a1,g1.(b1,c1)) = g1.(f1.(a1,b1),f1.(a1,c1))
proof let a1,b1,c1; consider a2,b2,c2;
[f1.(a1,g1.(b1,c1)),f2.(a2,g2.(b2,c2))] =
[g1.(f1.(a1,b1),f1.(a1,c1)),g2.(f2.(a2,b2),f2.(a2,c2))] by A5;
hence thesis by ZFMISC_1:33;
end;
let a2,b2,c2; consider a1,b1,c1;
[f1.(a1,g1.(b1,c1)),f2.(a2,g2.(b2,c2))] =
[g1.(f1.(a1,b1),f1.(a1,c1)),g2.(f2.(a2,b2),f2.(a2,c2))] by A5;
hence thesis by ZFMISC_1:33;
end;
theorem
Th29: 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 assume
A1: for b1,c1,a1 holds f1.(g1.(b1,c1),a1) = g1.(f1.(b1,a1),f1.(c1,a1));
defpred P[set,set,set] means
|:f1,f2:|.(|:g1,g2:|.($2,$3),$1) =
|:g1,g2:|.(|:f1,f2:|.($2,$1),|:f1,f2:|.($3,$1));
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 Th22
.= [f1.(g1.(b1,c1),a1),f2.(g2.(b2,c2),a2)] by Th22
.= [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 Th22
.= |:g1,g2:|.(|:f1,f2:|.([b1,b2],[a1,a2]),[f1.(c1,a1),f2.(c2,a2)])
by Th22
.= |:g1,g2:|.(|:f1,f2:|.([b1,b2],[a1,a2]),|:f1,f2:|.([c1,c2],[a1,a2]))
by Th22;
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 |:f1,f2:| is_right_distributive_wrt |:g1,g2:| by BINOP_1:def 19;
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 Th22
.= |:f1,f2:|.(|:g1,g2:|.([b1,b2],[c1,c2]),[a1,a2]) by Th22
.= |: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 Th22
.= |:g1,g2:|.([f1.(b1,a1),f2.(b2,a2)],[f1.(c1,a1),f2.(c2,a2)]) by Th22
.= [g1.(f1.(b1,a1),f1.(c1,a1)),g2.(f2.(b2,a2),f2.(c2,a2))] by Th22;
end;
thus for b1,c1,a1 holds f1.(g1.(b1,c1),a1) = g1.(f1.(b1,a1),f1.(c1,a1))
proof let b1,c1,a1; consider a2,b2,c2;
[f1.(g1.(b1,c1),a1),f2.(g2.(b2,c2),a2)] =
[g1.(f1.(b1,a1),f1.(c1,a1)),g2.(f2.(b2,a2),f2.(c2,a2))] by A5;
hence thesis by ZFMISC_1:33;
end;
let b2,c2,a2; consider a1,b1,c1;
[f1.(g1.(b1,c1),a1),f2.(g2.(b2,c2),a2)] =
[g1.(f1.(b1,a1),f1.(c1,a1)),g2.(f2.(b2,a2),f2.(c2,a2))] by A5;
hence thesis by ZFMISC_1:33;
end;
theorem
Th30: f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 iff
|:f1,f2:| is_distributive_wrt |:g1,g2:|
proof
thus f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 implies
|:f1,f2:| is_distributive_wrt |:g1,g2:|
proof assume
f1 is_left_distributive_wrt g1 & f1 is_right_distributive_wrt g1 &
f2 is_left_distributive_wrt g2 & f2 is_right_distributive_wrt g2;
hence |:f1,f2:| is_left_distributive_wrt |:g1,g2:| &
|:f1,f2:| is_right_distributive_wrt |:g1,g2:| by Th28,Th29;
end;
assume |:f1,f2:| is_left_distributive_wrt |:g1,g2:| &
|:f1,f2:| is_right_distributive_wrt |:g1,g2:|;
hence f1 is_left_distributive_wrt g1 & f1 is_right_distributive_wrt g1 &
f2 is_left_distributive_wrt g2 & f2 is_right_distributive_wrt g2
by Th28,Th29;
end;
theorem
Th31: 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,d1' being Element of D1,
d2,d2' being Element of D2 holds
P[[d1,d2],[d1',d2']]
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 Th22
.= [f1.(a1,g1.(a1,b1)),f2.(a2,g2.(a2,b2))] by Th22
.= [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 let a1,b1; consider a2,b2;
[a1,a2] = |:f1,f2:|.([a1,a2],|:g1,g2:|.([a1,a2],[b1,b2])) by A4
.= |:f1,f2:|.([a1,a2],[g1.(a1,b1),g2.(a2,b2)]) by Th22
.= [f1.(a1,g1.(a1,b1)),f2.(a2,g2.(a2,b2))] by Th22;
hence thesis by ZFMISC_1:33;
end;
let a2,b2; consider a1,b1;
[a1,a2] = |:f1,f2:|.([a1,a2],|:g1,g2:|.([a1,a2],[b1,b2])) by A4
.= |:f1,f2:|.([a1,a2],[g1.(a1,b1),g2.(a2,b2)]) by Th22
.= [f1.(a1,g1.(a1,b1)),f2.(a2,g2.(a2,b2))] by Th22;
hence thesis by ZFMISC_1:33;
end;
definition let L1,L2 be non empty LattStr;
func [:L1,L2:] -> strict LattStr equals:
Def7:
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;
definition let L1,L2 be non empty LattStr;
cluster [:L1,L2:] -> non empty;
coherence
proof [:L1,L2:] = 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:|#) by Def7;
hence the carrier of [:L1,L2:] is non empty;
end;
end;
definition let L be Lattice;
func LattRel L -> Relation equals:
Def8:
{ [p,q] where p is Element of L,
q is Element of L: p [= q };
coherence
proof
now let x; 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 st x = [x1,x2];
end; hence thesis by RELAT_1:def 1;
end;
end;
theorem
Th32: [p,q] in LattRel L iff p [= q
proof
A1: LattRel L = { [r,s]: r [= s } by Def8;
thus [p,q] in LattRel L implies p [= q
proof assume [p,q] in LattRel L;
then consider r,s such that
A2: [p,q] = [r,s] & r [= s by A1;
p = r & q = s by A2,ZFMISC_1:33;
hence thesis by A2;
end;
thus thesis by A1;
end;
theorem
Th33: dom LattRel L = the carrier of L &
rng LattRel L = the carrier of L & field LattRel L = the carrier of L
proof
A1: LattRel L = { [p,q]: p [= q } by Def8;
now let x;
thus x in the carrier of L implies ex y 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 by Th32;
hence thesis;
end;
given y such that
A2: [x,y] in LattRel L;
consider p,q such that
A3: [x,y] = [p,q] & p [= q by A1,A2;
x = p by A3,ZFMISC_1:33;
hence x in the carrier of L;
end;
hence
A4: dom LattRel L = the carrier of L by RELAT_1:def 4;
now let x;
thus x in the carrier of L implies ex y 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 by Th32;
hence thesis;
end;
given y such that
A5: [y,x] in LattRel L;
consider p,q such that
A6: [y,x] = [p,q] & p [= q by A1,A5;
x = q by A6,ZFMISC_1:33;
hence x in the carrier of L;
end;
hence rng LattRel L = the carrier of L by RELAT_1:def 5;
hence field LattRel L = (the carrier of L) \/ the carrier of L
by A4,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:48;
symmetry by WELLORD1:50;
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 by STRUCT_0:def 1;
join(L1) is commutative & join(L1) is associative &
meet(L1) is commutative & meet(L1) is associative &
join(L1) absorbs meet(L1) & meet(L1) absorbs join(L1) &
join(L2) is commutative & join(L2) is associative &
meet(L2) is commutative & meet(L2) is associative &
join(L2) absorbs meet(L2) & meet(L2) absorbs join(L2)
by LATTICE2:40,41;
then join(LL) is commutative & join(LL) is associative &
meet(LL) is commutative & meet(LL) is associative &
join(LL) absorbs meet(LL) & meet(LL) absorbs join(LL)
by Th23,Th24,Th31;
then LL is strict Lattice & LL = [:L1,L2:] by Def7,LATTICE2:17;
hence thesis;
end;
end;
theorem
for L1,L2,L3 being Lattice st L1,L2 are_isomorphic & L2,L3 are_isomorphic
holds L1,L3 are_isomorphic
proof let L1,L2,L3 be Lattice; assume
LattRel L1, LattRel L2 are_isomorphic &
LattRel L2, LattRel L3 are_isomorphic;
hence LattRel L1, LattRel L3 are_isomorphic by WELLORD1:52;
end;
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;
reconsider LL = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#)
as non empty LattStr by STRUCT_0:def 1;
[:L1,L2:] = LL by Def7;
then join(LL) is commutative & join(LL) is associative &
meet(LL) is commutative & meet(LL) is associative &
join(LL) absorbs meet(LL) & meet(LL) absorbs join(LL)
by A1,LATTICE2:27,29,31,32,40,41;
then join(L1) is commutative & join(L1) is associative &
meet(L1) is commutative & meet(L1) is associative &
join(L1) absorbs meet(L1) & meet(L1) absorbs join(L1) &
join(L2) is commutative & join(L2) is associative &
meet(L2) is commutative & meet(L2) is associative &
join(L2) absorbs meet(L2) & meet(L2) absorbs join(L2)
by Th23,Th24,Th31;
hence thesis by LATTICE2:17;
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:];
coherence
proof
[a,b] is Element of [:the carrier of L1, the carrier of L2:] &
[:L1,L2:] = 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:|#) by Def7;
hence thesis;
end;
end;
theorem
Th36: [p1,p2] "\/" [q1,q2] = [p1"\/"q1,p2"\/"q2] &
[p1,p2] "/\" [q1,q2] = [p1"/\"q1,p2"/\"q2]
proof
A1: [:L1,L2:] = 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:|#) by Def7;
thus [p1,p2] "\/" [q1,q2]
= join([:L1,L2:]).([p1,p2],[q1,q2]) by LATTICES:def 1
.= [join(L1).(p1,q1),join(L2).(p2,q2)] by A1,Th22
.= [p1"\/"q1,join(L2).(p2,q2)] by LATTICES:def 1
.= [p1"\/"q1,p2"\/"q2] by LATTICES:def 1;
thus [p1,p2] "/\" [q1,q2]
= meet([:L1,L2:]).([p1,p2],[q1,q2]) by LATTICES:def 2
.= [meet(L1).(p1,q1),meet(L2).(p2,q2)] by A1,Th22
.= [p1"/\"q1,meet(L2).(p2,q2)] by LATTICES:def 2
.= [p1"/\"q1,p2"/\"q2] by LATTICES:def 2;
end;
theorem
Th37: [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 Th36;
hence p1"\/"q1 = q1 & p2"\/"q2 = q2 by ZFMISC_1:33;
end;
assume p1"\/"q1 = q1 & p2"\/"q2 = q2;
hence [p1,p2] "\/" [q1,q2] = [q1,q2] by Th36;
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;
A4: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1), meet(L2):|#) by Def7;
then consider p1,p2 such that
A5: a = [p1,p2] by DOMAIN_1:9;
consider q1,q2 such that
A6: b = [q1,q2] by A4,DOMAIN_1:9;
consider r1,r2 such that
A7: c = [r1,r2] by A4,DOMAIN_1:9;
A8: p1 [= r1 & p2 [= r2 by A3,A5,A7,Th37;
thus a"\/"(b"/\"c) = a"\/"([q1"/\"r1,q2"/\"r2]) by A6,A7,Th36
.= [p1"\/"(q1"/\"r1),p2"\/"(q2"/\"r2)] by A5,Th36
.= [(p1"\/"q1)"/\"r1,p2"\/"(q2"/\"r2)] by A1,A8
.= [(p1"\/"q1)"/\"r1,(p2"\/"q2)"/\"r2] by A2,A8
.= [p1"\/"q1,p2"\/"q2]"/\"c by A7,Th36
.= (a"\/"b)"/\"c by A5,A6,Th36;
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 let p1,q1,r1 such that
A10: p1 [= r1;
consider p2,q2;
[p1,p2] [= [r1,p2] by A10,Th37;
then [p1,p2]"\/"([q1,q2]"/\"[r1,p2]) = ([p1,p2]"\/"[q1,q2])"/\"[r1,p2]
&
[q1,q2]"/\"[r1,p2] = [q1"/\"r1,q2"/\"p2] &
[p1,p2]"\/"[q1,q2] = [p1"\/"q1,p2"\/"q2] &
[p1,p2]"\/"[q1"/\"r1,q2"/\"p2] = [p1"\/"(q1"/\"r1),p2"\/"(q2"/\"p2)] &
[p1"\/"q1,p2"\/"q2]"/\"[r1,p2] = [(p1"\/"q1)"/\"r1,(p2"\/"q2)"/\"
p2] by A9,Th36;
hence thesis by ZFMISC_1:33;
end;
let p2,q2,r2 such that
A11: p2 [= r2;
consider p1,q1;
[p1,p2] [= [p1,r2] by A11,Th37;
then [p1,p2]"\/"([q1,q2]"/\"[p1,r2]) = ([p1,p2]"\/"[q1,q2])"/\"[p1,r2] &
[q1,q2]"/\"[p1,r2] = [q1"/\"p1,q2"/\"r2] &
[p1,p2]"\/"[q1,q2] = [p1"\/"q1,p2"\/"q2] &
[p1,p2]"\/"[q1"/\"p1,q2"/\"r2] = [p1"\/"(q1"/\"p1),p2"\/"(q2"/\"r2)] &
[p1"\/"q1,p2"\/"q2]"/\"[p1,r2] = [(p1"\/"q1)"/\"p1,(p2"\/"q2)"/\"
r2] by A9,Th36;
hence thesis by ZFMISC_1:33;
end;
theorem
Th39: L1 is D_Lattice & L2 is D_Lattice iff [:L1,L2:] is D_Lattice
proof
A1: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
thus L1 is D_Lattice & L2 is D_Lattice implies [:L1,L2:] is D_Lattice
proof assume L1 is D_Lattice & L2 is D_Lattice;
then join(L1) is_distributive_wrt meet(L1) &
join(L2) is_distributive_wrt meet(L2) by LATTICE2:35;
then |:join(L1),join(L2):| is_distributive_wrt |:meet(L1),meet(L2):|
by Th30;
hence thesis by A1,LATTICE2:36;
end;
assume [:L1,L2:] is D_Lattice;
then join([:L1,L2:]) is_distributive_wrt meet([:L1,L2:]) by LATTICE2:35;
then join(L1) is_distributive_wrt meet(L1) &
join(L2) is_distributive_wrt meet(L2) by A1,Th30;
hence thesis by LATTICE2:36;
end;
theorem
Th40: L1 is lower-bounded & L2 is lower-bounded
iff [:L1,L2:] is lower-bounded
proof
A1: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
thus L1 is lower-bounded & L2 is lower-bounded
implies [:L1,L2:] is lower-bounded
proof given p1 such that
A2: p1"/\"q1 = p1 & q1"/\"p1 = p1;
given p2 such that
A3: p2"/\"q2 = p2 & q2"/\"p2 = p2;
take a = [p1,p2]; let b be Element of [:L1,L2:];
consider q1,q2 such that
A4: b = [q1,q2] by A1,DOMAIN_1:9;
thus a"/\"b = [p1"/\"q1,p2"/\"q2] by A4,Th36 .= [p1,p2"/\"
q2] by A2 .= a by A3;
hence b"/\"a = a;
end;
given a being Element of [:L1,L2:] such that
A5: for b being Element of [:L1,L2:] holds
a"/\"b = a & b"/\"a = a;
consider p1,p2 such that
A6: a = [p1,p2] by A1,DOMAIN_1:9;
thus L1 is lower-bounded
proof take p1; let q1; consider q2;
a = a"/\"[q1,q2] by A5 .= [p1"/\"q1,p2"/\"q2] by A6,Th36;
hence thesis by A6,ZFMISC_1:33;
end;
take p2; let q2; consider q1;
a = a"/\"[q1,q2] by A5 .= [p1"/\"q1,p2"/\"q2] by A6,Th36;
hence thesis by A6,ZFMISC_1:33;
end;
theorem
Th41: L1 is upper-bounded & L2 is upper-bounded
iff [:L1,L2:] is upper-bounded
proof
A1: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
thus L1 is upper-bounded & L2 is upper-bounded
implies [:L1,L2:] is upper-bounded
proof given p1 such that
A2: p1"\/"q1 = p1 & q1"\/"p1 = p1;
given p2 such that
A3: p2"\/"q2 = p2 & q2"\/"p2 = p2;
take a = [p1,p2]; let b be Element of [:L1,L2:];
consider q1,q2 such that
A4: b = [q1,q2] by A1,DOMAIN_1:9;
thus a"\/"b = [p1"\/"q1,p2"\/"q2] by A4,Th36 .= [p1,p2"\/"
q2] by A2 .= a by A3;
hence b"\/"a = a;
end;
given a being Element of [:L1,L2:] such that
A5: for b being Element of [:L1,L2:] holds
a"\/"b = a & b"\/"a = a;
consider p1,p2 such that
A6: a = [p1,p2] by A1,DOMAIN_1:9;
thus L1 is upper-bounded
proof take p1; let q1; consider q2;
a = a"\/"[q1,q2] by A5 .= [p1"\/"q1,p2"\/"q2] by A6,Th36;
hence thesis by A6,ZFMISC_1:33;
end;
take p2; let q2; consider q1;
a = a"\/"[q1,q2] by A5 .= [p1"\/"q1,p2"\/"q2] by A6,Th36;
hence thesis by A6,ZFMISC_1:33;
end;
theorem
Th42: L1 is bounded & L2 is bounded
iff [:L1,L2:] is bounded
proof
thus L1 is bounded & L2 is bounded
implies [:L1,L2:] is bounded
proof assume
L1 is lower-bounded & L1 is upper-bounded &
L2 is lower-bounded & L2 is upper-bounded;
hence [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded
by Th40,Th41;
end;
assume [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded;
hence L1 is lower-bounded & L1 is upper-bounded &
L2 is lower-bounded & L2 is upper-bounded by Th40,Th41;
end;
theorem
Th43: L1 is 0_Lattice & L2 is 0_Lattice implies Bottom [:L1,L2:] = [Bottom L1,
Bottom L2]
proof assume
A1: L1 is 0_Lattice & L2 is 0_Lattice;
A2: now let a be Element of [:L1,L2:];
[:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
then consider p1,p2 such that
A3: a = [p1,p2] by DOMAIN_1:9;
thus [Bottom L1,Bottom L2]"/\"a = [Bottom L1"/\"p1,Bottom
L2"/\"p2] by A3,Th36 .= [Bottom L1,Bottom L2"/\"
p2] by A1,LATTICES:40
.= [Bottom L1,Bottom L2] by A1,LATTICES:40;
hence a"/\"[Bottom L1,Bottom L2]=[Bottom L1,Bottom L2];
end;
[:L1,L2:] is lower-bounded by A1,Th40;
hence Bottom [:L1,L2:] = [Bottom L1,Bottom L2] by A2,LATTICES:def 16;
end;
theorem
Th44: L1 is 1_Lattice & L2 is 1_Lattice implies Top [:L1,L2:] = [Top L1,Top
L2]
proof assume
A1: L1 is 1_Lattice & L2 is 1_Lattice;
then A2: [:L1,L2:] is upper-bounded by Th41;
now let a be Element of [:L1,L2:];
[:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
then consider p1,p2 such that
A3: a = [p1,p2] by DOMAIN_1:9;
thus [Top L1,Top L2]"\/"a = [Top L1"\/"p1,Top L2"\/"p2] by A3,Th36 .= [
Top L1,Top L2"\/"
p2] by A1,LATTICES:44
.= [Top L1,Top L2] by A1,LATTICES:44;
hence a"\/"[Top L1,Top L2] = [Top L1,Top L2];
end;
hence thesis by A2,LATTICES:def 17;
end;
theorem
Th45: 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
A1: L1 is 01_Lattice & 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 p1 is_a_complement_of q1 & p2 is_a_complement_of q2;
then A2: p1"\/"q1 = Top L1 & p1"/\"q1 = Bottom
L1 & p2"\/"q2 = Top L2 & p2"/\"q2 = Bottom L2
by LATTICES:def 18;
hence [p1,p2]"\/"[q1,q2] = [Top L1,Top L2] by Th36
.= Top [:L1,L2:] by A1,Th44;
hence [q1,q2]"\/"[p1,p2] = Top [:L1,L2:];
thus [p1,p2]"/\"[q1,q2] = [Bottom L1,Bottom L2] by A2,Th36
.= Bottom [:L1,L2:] by A1,Th43;
hence [q1,q2]"/\"[p1,p2] = Bottom [:L1,L2:];
end;
assume [p1,p2] is_a_complement_of [q1,q2];
then A3: [p1,p2]"\/"[q1,q2] = Top [:L1,L2:] & [p1,p2]"/\"[q1,q2] = Bottom [:L1
,L2:]
by LATTICES:def 18;
[Top L1,Top L2] = Top [:L1,L2:] by A1,Th44;
then A4: [Top L1,Top L2] = [p1"\/"q1,p2"\/"q2] by A3,Th36;
then A5: p1"\/"q1 = Top L1 by ZFMISC_1:33;
[Bottom L1,Bottom L2] = Bottom [:L1,L2:] by A1,Th43;
then A6: [p1"/\"q1,p2"/\"q2] = [Bottom L1,Bottom L2] by A3,Th36;
then p1"/\"q1 = Bottom L1 by ZFMISC_1:33;
hence p1 is_a_complement_of q1
by A5,LATTICES:def 18;
A7: p2"\/"q2 = Top L2 by A4,ZFMISC_1:33;
p2"/\"q2 = Bottom L2 by A6,ZFMISC_1:33;
hence p2 is_a_complement_of q2
by A7,LATTICES:def 18;
end;
theorem
Th46: L1 is C_Lattice & L2 is C_Lattice iff [:L1,L2:] is C_Lattice
proof
A1: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
thus L1 is C_Lattice & L2 is C_Lattice implies [:L1,L2:] is C_Lattice
proof assume
A2: L1 is C_Lattice & L2 is C_Lattice;
then reconsider L = [:L1,L2:] as 01_Lattice by Th42;
L is complemented
proof let a be Element of L;
consider p1,p2 such that
A3: a = [p1,p2] by A1,DOMAIN_1:9;
consider q1 such that
A4: q1 is_a_complement_of p1 by A2,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 A2,A3,A4,A5,Th45;
end;
hence thesis;
end;
assume
A6: [:L1,L2:] is C_Lattice;
then reconsider C1 = L1, C2 = L2 as 01_Lattice by Th42;
C1 is complemented
proof let p1' be Element of C1;
consider p2' being Element of C2;
reconsider p1 = p1' as Element of L1;
reconsider p2 = p2' 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 A1,DOMAIN_1:9;
reconsider q1' = q1 as Element of C1;
take q1';
thus thesis by A7,A8,Th45;
end;
hence L1 is C_Lattice;
C2 is complemented
proof let p2' be Element of C2;
consider p1' being Element of C1;
reconsider p1 = p1' as Element of L1;
reconsider p2 = p2' 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 A1,DOMAIN_1:9;
reconsider q2' = q2 as Element of C2;
take q2';
thus thesis by A9,A10,Th45;
end;
hence L2 is C_Lattice;
end;
theorem
L1 is B_Lattice & L2 is B_Lattice iff [:L1,L2:] is B_Lattice
proof
(L1 is B_Lattice iff L1 is C_Lattice & L1 is D_Lattice) &
(L2 is B_Lattice iff L2 is C_Lattice & L2 is D_Lattice) &
([:L1,L2:] is C_Lattice iff L1 is C_Lattice & L2 is C_Lattice) &
([:L1,L2:] is D_Lattice iff L1 is D_Lattice & L2 is D_Lattice) &
([:L1,L2:] is B_Lattice iff
[:L1,L2:] is C_Lattice & [:L1,L2:] is D_Lattice)
by Th39,Th46,LATTICES:def 20;
hence thesis;
end;
theorem
L1 is implicative & L2 is implicative
iff [:L1,L2:] is implicative
proof
A1: [:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1),meet(L2):|#) by Def7;
thus L1 is implicative & L2 is implicative
implies [:L1,L2:] is implicative
proof assume
A2: for p1,q1 ex r1 st p1"/\"r1 [= q1 &
for s1 st p1"/\"s1 [= q1 holds s1 [= r1;
assume
A3: 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
A4: a = [p1,p2] by A1,DOMAIN_1:9;
consider q1,q2 such that
A5: b = [q1,q2] by A1,DOMAIN_1:9;
consider r1 such that
A6: p1"/\"r1 [= q1 & for s1 st p1"/\"s1 [= q1 holds s1 [= r1 by A2;
consider r2 such that
A7: p2"/\"r2 [= q2 & for s2 st p2"/\"s2 [= q2 holds s2 [= r2 by A3;
take [r1,r2]; a"/\"[r1,r2] = [p1"/\"r1,p2"/\"r2] by A4,Th36;
hence a"/\"[r1,r2] [= b by A5,A6,A7,Th37;
let d be Element of [:L1,L2:];
consider s1,s2 such that
A8: d = [s1,s2] by A1,DOMAIN_1:9;
assume a"/\"d [= b; then [p1"/\"s1,p2"/\"s2] [= b by A4,A8,Th36;
then p1"/\"s1 [= q1 & p2"/\"s2 [= q2 by A5,Th37;
then s1 [= r1 & s2 [= r2 by A6,A7;
hence d [= [r1,r2] by A8,Th37;
end;
assume
A9: 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 let p1,q1; consider p2,q2;
consider c being Element of [:L1,L2:] such that
A10: [p1,p2]"/\"c [= [q1,q2] &
for d being Element of [:L1,L2:] st
[p1,p2]"/\"d [= [q1,q2] holds d [= c by A9;
consider r1,r2 such that
A11: c = [r1,r2] by A1,DOMAIN_1:9;
take r1; A12: [p1,p2]"/\"c = [p1"/\"r1,p2"/\"r2] by A11,Th36;
then A13: p1"/\"r1 [= q1 & p2"/\"r2 [= q2 by A10,Th37;
thus p1"/\"r1 [= q1 by A10,A12,Th37;
let s1; assume p1"/\"s1 [= q1;
then [p1"/\"s1,p2"/\"r2] [= [q1,q2] by A13,Th37;
then [p1,p2]"/\"[s1,r2] [= [q1,q2] by Th36;
then [s1,r2] [= c by A10;
hence s1 [= r1 by A11,Th37;
end;
let p2,q2; consider p1,q1;
consider c being Element of [:L1,L2:] such that
A14: [p1,p2]"/\"c [= [q1,q2] & for d being Element of [:L1,L2:]
st
[p1,p2]"/\"d [= [q1,q2] holds d [= c by A9;
consider r1,r2 such that
A15: c = [r1,r2] by A1,DOMAIN_1:9;
take r2; A16: [p1,p2]"/\"c = [p1"/\"r1,p2"/\"r2] by A15,Th36;
then A17: p1"/\"r1 [= q1 & p2"/\"r2 [= q2 by A14,Th37;
thus p2"/\"r2 [= q2 by A14,A16,Th37;
let s2; assume p2"/\"s2 [= q2;
then [p1"/\"r1,p2"/\"s2] [= [q1,q2] by A17,Th37;
then [p1,p2]"/\"[r1,s2] [= [q1,q2] by Th36;
then [r1,s2] [= c by A14;
hence s2 [= r2 by A15,Th37;
end;
theorem
[:L1,L2:].: = [:L1.:,L2.: :]
proof
[:L1,L2:] = LattStr (#[:the carrier of L1, the carrier of L2:],
|:join(L1), join(L2):|, |:meet(L1), meet(L2):|#) &
[:L1.:,L2.: :] = LattStr (#[:the carrier of L1.:, the carrier of L2.: :],
|:join(L1.:), join(L2.:):|, |:meet(L1.:), meet(L2.:):| #) &
L1.: = LattStr(#the carrier of L1, meet(L1), join(L1)#) &
L2.: = LattStr(#the carrier of L2, meet(L2), join(L2)#) &
[:L1,L2:].: = LattStr(#the carrier of [:L1,L2:],
meet([:L1,L2:]), join([:L1,L2:])#) by Def7,LATTICE2:def 2;
hence thesis;
end;
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: field R = the carrier of [:L1,L2:] &
field S = the carrier of [:L2,L1:] &
[:L1,L2:] = LattStr (#[:D1, D2:],
|:join(L1), join(L2):|, |:meet(L1), meet(L2):|#) &
[:L2,L1:] = LattStr (#[:D2, D1:],
|:join(L2), join(L1):|, |:meet(L2), meet(L1):|#) by Def7,Th33;
dom p1 = [:D1,D2:] & dom p2 = [:D1,D2:] by FUNCT_3:def 5,def 6;
then dom p2 /\ dom p1 = [:D1,D2:];
hence
A2: dom f = field R by A1,FUNCT_3:def 8;
rng p1 = D1 & rng p2 = D2 by FUNCT_3:60,62;
hence rng f c= field S by A1,FUNCT_3:71;
thus field S c= rng f
proof let x; assume x in field S;
then consider r2,r1 such that
A3: x = [r2,r1] by A1,DOMAIN_1:9;
f.[r1,r2] in rng f & f.[r1,r2] = [p2.[r1,r2],p1.[r1,r2]] &
p2.[r1,r2] = r2 & p1.[r1,r2] = r1
by A1,A2,FUNCT_1:def 5,FUNCT_3:def 5,def 6,def 8;
hence thesis by A3;
end;
thus f is one-to-one
proof let x,y; assume
A4: x in dom f; then consider r1,r2 such that
A5: x = [r1,r2] by A1,A2,DOMAIN_1:9;
assume
A6: y in dom f & f.x = f.y; then consider q1,q2 such that
A7: y = [q1,q2] by A1,A2,DOMAIN_1:9;
p1.[r1,r2] = r1 & p2.[r1,r2] = r2 & p1.[q1,q2] = q1 &
p2.[q1,q2] = q2 & f.x = [p2.x,p1.x] & f.y = [p2.y,p1.y]
by A4,A6,FUNCT_3:def 5,def 6,def 8;
then r1 = q1 & r2 = q2 by A5,A6,A7,ZFMISC_1:33;
hence thesis by A5,A7;
end;
A8: R = { [a,b] where a is Element of [:L1,L2:],
b is Element of [:L1,L2:]: a [= b } &
S = { [a,b] where a is Element of [:L2,L1:],
b is Element of [:L2,L1:]: a [= b }
by Def8;
let x,y;
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
A9: [x,y] = [a,b] & a [= b by A8;
consider r1,r2 such that
A10: a = [r1,r2] by A1,DOMAIN_1:9;
consider q1,q2 such that
A11: b = [q1,q2] by A1,DOMAIN_1:9;
A12: r1 [= q1 & r2 [= q2 by A9,A10,A11,Th37;
A13: x = a & y = b by A9,ZFMISC_1:33;
hence x in field R & y in field R by A1;
[r2,r1] [= [q2,q1] & p1.x = r1 & p2.x = r2 & p1.y = q1 & p2.y = q2 &
f.x = [p2.x,p1.x] & f.y = [p2.y,p1.y]
by A1,A2,A10,A11,A12,A13,Th37,FUNCT_3:def 5,def 6,def 8;
hence thesis by A8;
end;
assume
A14: x in field R & y in field R;
then consider r1,r2 such that
A15: x = [r1,r2] by A1,DOMAIN_1:9;
consider q1,q2 such that
A16: y = [q1,q2] by A1,A14,DOMAIN_1:9;
assume
A17: [f.x,f.y] in S;
f.[r1,r2] = [p2.[r1,r2],p1.[r1,r2]] & p1.[r1,r2] = r1 & p2.[r1,r2] = r2 &
f.[q1,q2] = [p2.[q1,q2],p1.[q1,q2]] & p1.[q1,q2] = q1 & p2.[q1,q2] = q2
by A1,A2,FUNCT_3:def 5,def 6,def 8;
then [r2,r1] [= [q2,q1] by A15,A16,A17,Th32;
then r2 [= q2 & r1 [= q1 by Th37;
then [r1,r2] [= [q1,q2] by Th37;
hence [x,y] in R by A15,A16,Th32;
end;
reserve B for B_Lattice,
a,b,c,d for Element of B;
theorem
Th51: a <=> b = (a"/\"b)"\/"(a`"/\"b`)
proof
thus a <=> b = (a => b)"/\"(b => a) by FILTER_0:def 11
.= (a`"\/"b)"/\"(b => a) by FILTER_0:55
.= (a`"\/"b)"/\"(b`"\/"a) by FILTER_0:55
.= (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:47
.= ((a`"/\"b`)"\/"Bottom B)"\/"(Bottom B"\/"(b"/\"a)) by LATTICES:47
.= (a`"/\"b`)"\/"(Bottom B"\/"(b"/\"a)) by LATTICES:39
.= (a"/\"b)"\/"(a`"/\"b`) by LATTICES:39;
end;
theorem
Th52: (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:55 .= a`` "/\" b` by LATTICES:51
.= a "/\" b` by LATTICES:49;
end;
hence (a => b)` = a "/\" b`;
thus (a <=> b)` = ((a=>b)"/\"(b=>a))` by FILTER_0:def 11
.= (a=>b)`"\/"(b=>a)` by LATTICES:50
.= (a"/\"b`)"\/"(b=>a)` by A1 .= (a"/\"b`)"\/"(a`"/\"b) by A1;
hence (a <=> b)` = (a"/\"b`)"\/"(a`"/\"b``) by LATTICES:49
.= a <=> b` by Th51;
hence (a <=> b)` = (a"/\"b`)"\/"(a`"/\"b``) by Th51
.= (a``"/\"b`)"\/"(a`"/\"b``) by LATTICES:49
.= (a`"/\"b)"\/"(a``"/\"b`) by LATTICES:49
.= a` <=> b by Th51;
end;
theorem
Th53: a <=> b = a <=> c implies b = c
proof
set ab = a"/\"b; set ac = a"/\"c;
set bc = b"/\"c; set b'c' = b`"/\"c`;
set a'b' = a`"/\"b`; set a'c' = a`"/\"c`;
set a'b = a`"/\"b; set a'c = a`"/\"c;
set ab' = a"/\"b`; set ac' = a"/\"c`;
A1: (a<=>b) <=> (a<=>c) = ((a<=>b)"/\"(a<=>c))"\/"((a<=>b)`"/\"(a<=>c)`) &
a<=>b = ab"\/"a'b' & a<=>c = ac"\/"a'c' & (a<=>b)` = ab'"\/"a'b &
(a<=>c)` = ac'"\/"a'c &
(ab"\/"a'b')"/\"(ac"\/"a'c') = (ab"/\"(ac"\/"a'c'))"\/"(a'b'"/\"(ac"\/"
a'c')) &
ab"/\"(ac"\/"a'c') = (ab"/\"ac)"\/"(ab"/\"a'c') & ab"/\"a'c' = ab"/\"a`"/\"
c` &
a'b'"/\"(ac"\/"a'c') = (a'b'"/\"ac)"\/"(a'b'"/\"a'c') & b"/\"a"/\"a` = b
"/\"(a"/\"a`) &
b"/\"Bottom B = Bottom B & b`"/\"Bottom B = Bottom B & Bottom B"/\"c =
Bottom B & Bottom B"/\"c` = Bottom B &
a"/\"a` = Bottom B & a`"/\"a = Bottom B & ab = b"/\"a & a'b' = b`"/\"a` &
a'b'"/\"ac = a'b'"/\"a"/\"c & b`"/\"a`"/\"a = b`"/\"(a`"/\"a) &
(ab"/\"ac)"\/"Bottom B = ab"/\"ac & Bottom
B"\/"(a'b'"/\"a'c') = a'b'"/\"a'c' &
(ab'"\/"a'b)"/\"(ac'"\/"a'c) = (ab'"/\"(ac'"\/"a'c))"\/"(a'b"/\"(ac'"\/"
a'c)) &
ab'"/\"(ac'"\/"a'c) = (ab'"/\"ac')"\/"(ab'"/\"a'c) & ab'"/\"a'c = ab'"/\"a`
"/\"c &
a'b"/\"(ac'"\/"a'c) = (a'b"/\"ac')"\/"(a'b"/\"a'c) & b`"/\"a"/\"a` = b`"/\"
(a"/\"a`) &
b`"/\"Bottom B = Bottom B & b"/\"Bottom B = Bottom B & Bottom B"/\"c` =
Bottom B & Bottom B"/\"c = Bottom B &
a"/\"a` = Bottom B & a`"/\"a = Bottom B & ab' = b`"/\"a & a'b = b"/\"a` &
a'b"/\"ac' = a'b"/\"a"/\"c` & b"/\"a`"/\"a = b"/\"(a`"/\"a) &
(ab'"/\"ac')"\/"Bottom B = ab'"/\"ac' & Bottom
B"\/"(a'b"/\"a'c) = a'b"/\"a'c
by Th51,Th52,LATTICES:39,40,47,def 7,def 11;
ab"/\"ac = ab"/\"a"/\"c & ab"/\"a = a"/\"ab & a"/\"ab = a"/\"a"/\"b & a
"/\"
a = a &
a'b'"/\"a'c' = a'b'"/\"a`"/\"c` & a'b'"/\"a` = a`"/\"a'b' & a`"/\"a'b' = a`
"/\"a`"/\"b` &
a`"/\"a` = a` & ab'"/\"ac' = ab'"/\"a"/\"c` & ab'"/\"a = a"/\"ab' & (a"/\"b
"/\"c) = a"/\"bc &
a"/\"ab' = a"/\"a"/\"b` & a'b"/\"a'c = a'b"/\"a`"/\"c & a'b"/\"a` = a`"/\"
a'b &
(a`"/\"b"/\"c) = a`"/\"bc & (a"/\"b`"/\"c`) = a"/\"b'c' & (a`"/\"b`"/\"c`)
= a`"/\"b'c' & a`"/\"a'b = a`"/\"a`"/\"b &
(a"/\"bc)"\/"(a`"/\"b'c')"\/"((a"/\"b'c')"\/"(a`"/\"bc)) =
(a"/\"bc)"\/"(a`"/\"b'c')"\/"(a"/\"b'c')"\/"(a`"/\"bc) &
(a"/\"bc)"\/"(a`"/\"b'c')"\/"(a"/\"b'c') = (a"/\"b'c')"\/"((a"/\"bc)"\/"(a`
"/\"b'c')) &
(a"/\"b'c')"\/"((a"/\"bc)"\/"(a`"/\"b'c')) = (a"/\"b'c')"\/"(a"/\"bc)"\/"
(a`"/\"b'c') &
(a"/\"b'c')"\/"(a"/\"bc) = a"/\"(b'c'"\/"bc) & b'c'"\/"bc = bc"\/"b'c' &
(a`"/\"b'c')"\/"(a`"/\"bc) = a`"/\"(b'c'"\/"bc) & (Top B)"/\"(b'c'"\/"
bc) = b'c'"\/"bc &
(a"/\"(b'c'"\/"bc))"\/"(a`"/\"b'c')"\/"(a`"/\"bc) =
(a"/\"(b'c'"\/"bc))"\/"((a`"/\"b'c')"\/"(a`"/\"bc)) & a"\/"a` = Top B &
(a"/\"(b'c'"\/"bc))"\/"(a`"/\"(b'c'"\/"bc)) = (a"\/"a`)"/\"(b'c'"\/"bc)
by LATTICES:18,43,48,def 5,def 7,def 11;
then A2: (a<=>b) <=> (a<=>c) = b <=> c & B is I_Lattice by A1,Th51,FILTER_0:40
;
assume a<=>b = a<=>c;
then (a<=>b) => (a<=>c) = Top B & (a<=>c) => (a<=>b) = Top
B by A2,FILTER_0:38;
then b <=> c = Top B"/\"Top B by A2,FILTER_0:def 11 .= Top
B by LATTICES:18;
then (b => c)"/\"(c => b) = Top B & (b => c)"/\"(c => b) = (c => b)"/\"(b
=> c)
by FILTER_0:def 11;
then Top B [= b => c & Top B [= c => b by LATTICES:23;
then b"/\"Top B [= b"/\"(b => c) & c"/\"Top
B [= c"/\"(c => b) & b"/\"(b => c) [= c &
c"/\"(c => b) [= b & b"/\"Top B = b & c"/\"Top B = c
by A2,FILTER_0:def 8,LATTICES:27,43;
then b [= c & c [= b by LATTICES:25;
hence thesis by LATTICES:26;
end;
theorem
Th54: a <=> (a <=> b) = b
proof
a<=>(a<=>b) = (a"/\"(a<=>b))"\/"(a`"/\"(a<=>b)`) &
a<=>b = (a"/\"b)"\/"(a`"/\"b`) & (a<=>b)` = (a"/\"b`)"\/"(a`"/\"b) &
a"/\"((a"/\"b)"\/"(a`"/\"b`)) = (a"/\"(a"/\"b))"\/"(a"/\"(a`"/\"b`)) &
a`"/\"((a"/\"b`)"\/"(a`"/\"b)) = (a`"/\"(a"/\"b`))"\/"(a`"/\"(a`"/\"b)) &
a"/\"(a"/\"b) = a"/\"a"/\"b & a`"/\"(a"/\"b`) = a`"/\"a"/\"b` & a"/\"
a = a & a`"/\"a` = a` &
a`"/\"(a`"/\"b) = a`"/\"a`"/\"b & a"/\"(a`"/\"b`) = a"/\"a`"/\"b` & Bottom
B"/\"
b = Bottom B &
a"/\"a` = Bottom B & a`"/\"a = Bottom B & (a"/\"b)"\/"Bottom B = a"/\"b &
Bottom B"\/"(a`"/\"
b) = a`"/\"b &
(a"/\"b)"\/"(a`"/\"b) = (a"\/"a`)"/\"b & a"\/"a` = Top B & Top
B"/\"b = b & Bottom B
"/\"b` = Bottom B
by Th51,Th52,LATTICES:18,39,40,43,47,48,def 7,def 11;
hence thesis;
end;
theorem
(i"\/"j) => i = j => i & i => (i"/\"j) = i => j
proof
j=>i [= (j=>i)"\/"i & i"\/"(j=>i) = (j=>i)"\/"i & j"/\"(j=>i) [= i &
i"\/"i = i by FILTER_0:def 8,LATTICES:17,22;
then i"\/"(j"/\"(j=>i)) [= i & i"\/"(j"/\"(j=>i)) = (i"\/"j)"/\"(i"\/"(j=>
i)) &
(i"\/"j)"/\"(j=>i) [= (i"\/"j)"/\"(i"\/"
(j=>i)) by FILTER_0:1,LATTICES:27,31;
then (i"\/"j)"/\"(j=>i) [= i & j [= j"\/"i & i"\/"j = j"\/"
i by LATTICES:22,25;
then A1: j=>i [= (i"\/"j)=>i & (i"\/"j)"/\"((i"\/"j)=>i) [= i &
j"/\"((i"\/"j)=>i) [= (i"\/"j)"/\"((i"\/"
j)=>i) by FILTER_0:def 8,LATTICES:27;
then j"/\"((i"\/"j)=>i) [= i by LATTICES:25;
then (i"\/"j)=>i [= j=>i by FILTER_0:def 8;
hence (i"\/"j) => i = j => i by A1,LATTICES:26;
i"/\"(i=>(i"/\"j)) [= i"/\"j & j"/\"i [= j & i"/\"j = j"/\"i
by FILTER_0:def 8,LATTICES:23;
then i"/\"(i=>(i"/\"j)) [= j by LATTICES:25;
then A2: i=>(i"/\"j) [= i=>j by FILTER_0:def 8;
i"/\"(i=>j) [= j by FILTER_0:def 8;
then i"/\"(i"/\"(i=>j)) [= i"/\"j & i"/\"(i"/\"(i=>j)) = i"/\"i"/\"(i=>j)
& i
"/\"i = i
by LATTICES:18,27,def 7;
then i=>j [= i=>(i"/\"j) by FILTER_0:def 8;
hence thesis by A2,LATTICES:26;
end;
theorem
Th56: 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 & j [= j"\/"k & i"/\"k [= i
by FILTER_0:def 8,LATTICES:22,23;
then A2: i"/\"(i=>j) [= j"\/"k & (i"/\"k)"/\"(i=>j) [= i"/\"
(i=>j) by LATTICES:25,27;
then (i"/\"k)"/\"(i=>j) [= j by A1,LATTICES:25;
hence thesis by A2,FILTER_0:def 8;
end;
Lm1: i => j in F_I implies i => (j"\/"k) in F_I & i => (k"\/"j) in F_I &
(i"/\"k) => j in F_I & (k"/\"i) => j in F_I
proof
i => j [= i => (j"\/"k) & i => j [= (i"/\"k) => j &
i => j [= i => (k"\/"j) & i => j [= (k"/\"i) => j by Th56;
hence thesis by FILTER_0:9;
end;
theorem
Th57: (i => k)"/\"(j => k) [= (i"\/"j) => k
proof i"/\"(i=>k) [= k & j"/\"(j=>k) [= k by FILTER_0:def 8;
then i"/\"(i=>k)"/\"(j=>k) [= k & j"/\"(j=>k)"/\"(i=>k) [= k &
i"/\"((i=>k)"/\"(j=>k)) = i"/\"(i=>k)"/\"(j=>k) &
(i"/\"((i=>k)"/\"(j=>k)))"\/"(j"/\"((i=>k)"/\"(j=>k))) = (i"\/"j)"/\"
((i=>k)"/\"(j=>k)) &
(j=>k)"/\"(i=>k) = (i=>k)"/\"(j=>k) & j"/\"((j=>k)"/\"(i=>k)) = j"/\"(j=>k)
"/\"(i=>k)
by FILTER_0:2,LATTICES:def 7,def 11;
then (i"\/"j)"/\"((i=>k)"/\"(j=>k)) [= k by FILTER_0:6;
hence (i=>k)"/\"(j=>k) [= (i"\/"j)=> k by FILTER_0:def 8;
end;
Lm2: i => k in F_I & j => k in F_I implies (i"\/"j) => k in F_I
proof
A1: (i=>k)"/\"(j=>k) [= (i"\/"j)=> k by Th57;
assume i => k in F_I & j => k in F_I;
then (i=>k)"/\"(j=>k) in F_I by FILTER_0:def 1;
hence thesis by A1,FILTER_0:9;
end;
theorem
Th58: (i => j)"/\"(i => k) [= i => (j"/\"k)
proof i"/\"(i=>k) [= k & i"/\"(i=>j) [= j by FILTER_0:def 8;
then (i"/\"(i=>j))"/\"(i"/\"(i=>k)) [= j"/\"k & i"/\"i = i &
(i"/\"(i=>j))"/\"(i"/\"(i=>k)) = ((i"/\"(i=>j))"/\"i)"/\"(i=>k) &
(i"/\"(i=>j))"/\"i = i"/\"(i"/\"(i=>j)) & i"/\"(i"/\"(i=>j)) = i"/\"i"/\"
(i=>j) &
i"/\"((i=>j)"/\"(i=>k)) = i"/\"(i=>j)"/\"
(i=>k) by FILTER_0:5,LATTICES:18,def 7;
hence (i=>j)"/\"(i=>k) [= i=>(j"/\"k) by FILTER_0:def 8;
end;
Lm3: i => j in F_I & i => k in F_I implies i => (j"/\"k) in F_I
proof
A1: (i=>j)"/\"(i=>k) [= i=>(j"/\"k) by Th58;
assume i => j in F_I & i => k in F_I;
then (i=>j)"/\"(i=>k) in F_I by FILTER_0:def 1;
hence thesis by A1,FILTER_0:9;
end;
theorem
Th59: i1 <=> i2 in F_I & j1 <=> j2 in F_I implies
(i1"\/"j1) <=> (i2"\/"j2) in F_I & (i1"/\"j1) <=> (i2"/\"j2) in F_I
proof assume
A1: i1 <=> i2 in F_I & j1 <=> j2 in F_I;
i1 <=> i2 = (i1=>i2)"/\"(i2=>i1) & j1 <=> j2 = (j1=>j2)"/\"(j2=>j1)
by FILTER_0:def 11;
then i1=>i2 in F_I & i2=>i1 in F_I & j1=>j2 in F_I & j2=>j1 in F_I
by A1,FILTER_0:def 1;
then (i1"/\"j1)=>i2 in F_I & (i1"/\"j1)=>j2 in F_I &
(i2"/\"j2)=>i1 in F_I & (i2"/\"j2)=>j1 in F_I &
i1=>(i2"\/"j2) in F_I & j1=>(i2"\/"j2) in F_I &
i2=>(i1"\/"j1) in F_I & j2=>(i1"\/"j1) in F_I by Lm1;
then (i1"/\"j1) => (i2"/\"j2) in F_I & (i2"/\"j2) => (i1"/\"j1) in F_I &
(i1"/\"j1) <=> (i2"/\"j2) = ((i1"/\"j1)=>(i2"/\"j2))"/\"((i2"/\"j2)=>(i1
"/\"j1)) &
(i1"\/"j1) => (i2"\/"j2) in F_I & (i2"\/"j2) => (i1"\/"j1) in F_I &
(i1"\/"j1) <=> (i2"\/"j2) = ((i1"\/"j1)=>(i2"\/"j2))"/\"((i2"\/"j2)=>(i1
"\/"j1))
by Lm2,Lm3,FILTER_0:def 11;
hence thesis by FILTER_0:def 1;
end;
Lm4: i in Class(equivalence_wrt F_I,j) iff i <=> j in F_I
proof
(i in Class(equivalence_wrt F_I,j) iff [i,j] in equivalence_wrt F_I) &
([i,j] in equivalence_wrt F_I iff i <=> j in F_I)
by EQREL_1:27,FILTER_0:def 12;
hence thesis;
end;
theorem Th60:
i in Class(equivalence_wrt F_I,k) & j in Class(equivalence_wrt F_I,k) implies
i"\/"j in Class(equivalence_wrt F_I,k) & i"/\"
j in Class(equivalence_wrt F_I,k)
proof assume
i in Class(equivalence_wrt F_I,k) & j in Class(equivalence_wrt F_I,k);
then i <=> k in F_I & j <=> k in F_I & k"\/"k = k & k"/\"k = k
by Lm4,LATTICES:17,18;
then (i"\/"j) <=> k in F_I & (i"/\"j) <=> k in F_I by Th59;
hence thesis by Lm4;
end;
theorem
Th61: 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: B is I_Lattice by FILTER_0:40;
d in <.d.) & c <=>(c <=>d) = d & (c <=>d)<=>c = c <=>(c <=>d)
by Th54,FILTER_0:19,77;
then c <=>d in A & c in A by A1,Lm4,EQREL_1:28;
hence (c"\/"(c <=>d)) in A by A1,Th60;
let b; assume b in A;
then b<=>c in <.d.) by A1,Lm4;
then d [= b<=>c & (b<=>c)` = (b"/\"c`)"\/"(b`"/\"c) by Th52,FILTER_0:18;
then (b"/\"c`)"\/"(b`"/\"c) [= d` by LATTICES:53;
then ((b"/\"c`)"\/"(b`"/\"c))"/\"c` [= d`"/\"c` & (b"/\"c`)"/\"c`= b"/\"(c
`"/\"
c`) & c` = c`"/\"c` &
((b"/\"c`)"\/"(b`"/\"c))"/\"c` = ((b"/\"c`)"/\"c`)"\/"((b`"/\"c)"/\"c`) & b
"/\"c`"\/"Bottom B = b"/\"c` &
(b`"/\"c)"/\"c`= b`"/\"(c"/\"c`) & Bottom
B = c"/\"c` & d`"/\"c` = c`"/\"d` & c
"/\"b [= c &
c"/\"b = b"/\"c & c"/\"d [= c & (c"/\"d)"\/"c = c"\/"(c"/\"d) & b`"/\"
Bottom B = Bottom B
by LATTICES:18,23,27,39,40,47,def 7,def 11;
then (b"/\"c`)"\/"(b"/\"c) [= (c`"/\"d`)"\/"(b"/\"c) & (b"/\"c`)"\/"(b"/\"
c) = b
"/\"(c`"\/"c) &
c`"\/"c = Top B & b"/\"Top
B = b & (c`"/\"d`)"\/"(b"/\"c) [= (c`"/\"d`)"\/"c &
(c`"/\"d`)"\/"c = c"\/"(c`"/\"d`) & c = c"\/"(c"/\"d) & (c"/\"d)"\/"(c`"/\"
d`) = c <=>d &
c"\/"(c"/\"d)"\/"(c`"/\"d`) = c"\/"((c"/\"d)"\/"(c`"/\"d`))
by Th51,FILTER_0:1,LATTICES:43,48,def 5,def 8,def 11;
hence thesis by LATTICES:25;
end;
theorem
B, [:B/\/<.a.),latt <.a.):] are_isomorphic
proof set F = <.a.); set E = equivalence_wrt F;
A1: B is 0_Lattice & B is 1_Lattice & B is I_Lattice
by FILTER_0:40;
deffunc F(set) = Class(E,$1);
consider g being Function such that
A2: dom g = the carrier of B & for x st x in the carrier of B holds
g.x = F(x) from Lambda;
A3: (b"\/"(b<=>a)) <=> b = b"\/"a
proof
(b"\/"(b<=>a)) <=> b = ((b"\/"(b<=>a))"/\"b)"\/"((b"\/"(b<=>a))`"/\"
b`) &
(b"\/"(b<=>a))` = b`"/\"(b<=>a)` & (b<=>a)` = (b"/\"a`)"\/"(b`"/\"a) &
b`"/\"((b"/\"a`)"\/"(b`"/\"a)) = (b`"/\"(b"/\"a`))"\/"(b`"/\"(b`"/\"
a)) &
b`"/\"(b"/\"a`) = b`"/\"b"/\"a` & b`"/\"b = Bottom
B & b`"/\"(b`"/\"a) = b`
"/\"b`"/\"a &
b`"/\"b` = b` & Bottom B"/\"a` = Bottom B & Bottom
B"\/"(b`"/\"a) = b`"/\"a &
b`"/\"(b`"/\"a) = b`"/\"a"/\"b` &
b<=>a = (b"/\"a)"\/"(b`"/\"a`) & b"\/"((b"/\"a)"\/"(b`"/\"a`)) = b"\/"(b
"/\"a)"\/"(b`"/\"a`) &
b"\/"(b"/\"a) = (b"/\"a)"\/"b & (b"/\"a)"\/"b = b &
(b"\/"(b`"/\"a`))"/\"b = (b"/\"b)"\/"(b`"/\"a`"/\"b) & b`"/\"(a`"/\"
b) = b`"/\"a`"/\"b &
a`"/\"b = b"/\"a` & b"/\"b = b & b"\/"Bottom B = b
by Th51,Th52,LATTICES:18,39,40,47,51,def 5,def 7,def 8,def 11;
hence (b"\/"(b<=>a)) <=> b = b"\/"((b"/\"a)"\/"(b`"/\"
a)) by LATTICES:def 5
.= b"\/"((b"\/"b`)"/\"a) by LATTICES:def 11
.= b"\/"(Top B"/\"a) by LATTICES:48
.= b"\/"a by LATTICES:43;
end;
A4: the carrier of latt F = F by FILTER_0:63;
deffunc F(Element of B) = ($1"\/"($1<=>a)) <=> $1;
consider h being UnOp of the carrier of B such that
A5: h.b = F(b) from LambdaD;
take f = <:g,h:>; set R = LattRel B; set S = LattRel [:B/\/F,latt F:];
A6: field R = the carrier of B &
field S = the carrier of [:B/\/F,latt F:] by Th33;
A7: dom h = dom g by A2,FUNCT_2:def 1;
hence
A8: dom f = field R by A2,A6,FUNCT_3:70;
reconsider o1 = join(B), o2 = meet(B) as BinOp of E by A1,Th13,Th14;
A9: the carrier of latt F = F &
LattStr(#Class E,o1/\/E,o2/\/E#) = B/\/F by A1,Def5,FILTER_0:63;
A10: h.b is Element of latt F
proof b"\/"(b<=>a) in Class(E,b) by Th61;
then [b"\/"(b<=>a),b] in E by EQREL_1:27;
then h.b = (b"\/"(b<=>a)) <=> b & (b"\/"(b<=>a)) <=> b in F
by A5,FILTER_0:def 12;
hence thesis by FILTER_0:63;
end;
A11: [:B/\/F, latt F:] = LattStr (#[:carr(B/\/F), carr(latt F):],
|:join(B/\/F),join(latt F):|,|:meet(B/\/F),meet(latt F):|#)
by Def7;
thus rng f c= field S
proof let x; assume x in rng f;
then consider y such that
A12: y in dom f & x = f.y by FUNCT_1:def 5;
reconsider y as Element of B by A2,A7,A12,FUNCT_3:70;
g.y = Class(E,y) by A2;
then reconsider z1 = g.y as Element of B/\/F by A9;
reconsider z2 = h.y as Element of latt F by A10;
x = [z1,z2] by A12,FUNCT_3:def 8;
hence thesis by A6;
end;
thus field S c= rng f
proof let x; assume x in field S;
then consider y being Element of Class E,
z being Element of F such that
A13: x = [y,z] by A6,A9,A11,DOMAIN_1:9;
consider b such that
A14: y = Class(E,b) by EQREL_1:45;
set ty = b"\/"(b<=>a);
A15: ty in y by A14,Th61;
then A16: y = Class(E,ty) by A14,EQREL_1:31;
ty <=> (ty <=> z) = z by Th54;
then (ty <=> z) <=> ty = z by FILTER_0:77;
then [ty <=> z,ty] in E by FILTER_0:def 12;
then A17: ty <=> z in y by A16,EQREL_1:27;
then A18: y = Class(E,ty<=>z) by A14,EQREL_1:31;
then (ty<=>z)"\/"((ty<=>z)<=>a) in y by Th61;
then (ty<=>z)"\/"((ty<=>z)<=>a) [= ty & ty [= (ty<=>z)"\/"((ty<=>z)<=>a
)
by A14,A15,A18,Th61;
then h.(ty<=>z) = ((ty<=>z)"\/"((ty<=>z)<=>a)) <=> (ty<=>z) &
(ty<=>z)"\/"((ty<=>z)<=>a) = ty &
y = Class(E,ty<=>z) by A5,A14,A17,EQREL_1:31,LATTICES:26;
then g.(ty <=> z) = y & h.(ty <=> z) = z by A2,Th54;
then x = f.(ty <=> z) by A6,A8,A13,FUNCT_3:def 8;
hence thesis by A6,A8,FUNCT_1:def 5;
end;
thus f is one-to-one
proof let x,y; assume x in dom f & y in dom f;
then reconsider x' = x, y' = y as Element of B by A2,A7,
FUNCT_3:70;
A19: f.x = [g.x',h.x'] & f.y = [g.y',h.y'] & g.x' = Class(E,x') &
g.y' = Class(E,y') & h.x' = (x'"\/"(x'<=>a)) <=> x' &
x'"\/"(x'<=>a) in Class(E,x') & y'"\/"(y'<=>a) in Class(E,y') &
h.y' = (y'"\/"(y'<=>a)) <=> y' by A2,A5,A6,A8,Th61,FUNCT_3:def 8;
assume f.x = f.y;
then A20: g.x = g.y & h.x = h.y by A19,ZFMISC_1:33;
then x'"\/"(x'<=>a) [= y'"\/"(y'<=>a) & y'"\/"(y'<=>a) [= x'"\/"(x'<=>a
)
by A19,Th61;
then y'"\/"(y'<=>a) = x'"\/"(x'<=>a) by LATTICES:26;
hence x = y by A19,A20,Th53;
end;
let x,y;
thus [x,y] in R implies x in field R & y in field R & [f.x,f.y] in S
proof assume
A21: [x,y] in R;
hence x in field R & y in field R by RELAT_1:30;
reconsider x' = x, y' = y as Element of B
by A6,A21,RELAT_1:30;
A22: x' [= y' & x'"/\"Top B = x' by A21,Th32,LATTICES:43;
then Top B [= x' => y' & Top B in F by A1,FILTER_0:12,def 8;
then x' => y' in F by FILTER_0:9;
then A23: x'/\/F [= y'/\/F & x'/\/F = Class(E,x') & Class(E,x') = g.x' &
y'/\/F = Class(E,y') & Class(E,y') = g.y' by A1,A2,Def6,Th16;
A24: h.x' = (x'"\/"(x'<=>a)) <=> x' & h.y' = (y'"\/"(y'<=>a)) <=> y' &
f.x' = [g.x',h.x'] & f.y' = [g.y',h.y'] & x'"\/"a [= y'"\/"a &
(x'"\/"(x'<=>a)) <=> x' = x'"\/"a & (y'"\/"(y'<=>a)) <=> y' = y'"\/"a
by A3,A5,A6,A8,A22,FILTER_0:1,FUNCT_3:def 8;
x'"\/"(x'<=>a) in Class(E,x') & y'"\/"
(y'<=>a) in Class(E,y') by Th61;
then reconsider hx = h.x, hy = h.y as Element of latt F
by A1,A4,A24,Lm4;
hx [= hy by A24,FILTER_0:65;
then [x'/\/F,hx] [= [y'/\/F,hy] by A23,Th37;
hence thesis by A23,A24,Th32;
end;
assume x in field R & y in field R;
then reconsider x' = x, y' = y as Element of B by Th33;
A25: x'/\/F = Class(E,x') & y'/\/F = Class(E,y') &
Class(E,x') = g.x' & Class(E,y') = g.y' &
h.x' = (x'"\/"(x'<=>a)) <=> x' & h.y' = (y'"\/"(y'<=>a)) <=> y' &
f.x' = [g.x',h.x'] & f.y' = [g.y',h.y'] &
(x'"\/"(x'<=>a)) <=> x' = x'"\/"a & (y'"\/"(y'<=>a)) <=> y' = y'"\/"a
by A1,A2,A3,A5,A6,A8,Def6,FUNCT_3:def 8;
x'"\/"(x'<=>a) in Class(E,x') & y'"\/"(y'<=>a) in Class(E,y') by Th61;
then reconsider hx = h.x, hy = h.y as Element of latt F
by A1,A4,A25,Lm4;
assume [f.x,f.y] in S;
then [x'/\/F,hx] [= [y'/\/F,hy] by A25,Th32;
then x'/\/F [= y'/\/F & hx [= hy by Th37;
then x' => y' in F & x' => y' = x'`"\/"y' & x'"\/"a [= y'"\/"a & x' [= x'
"\/"a
by A1,A25,Th16,FILTER_0:55,65,LATTICES:22;
then a [= x'`"\/"y' & x'"/\"(x'"\/"a) [= x'"/\"(y'"\/"a) & x'"/\"(x'"\/"a)
= x'
by FILTER_0:18,LATTICES:21,27;
then A26: x'"/\"a [= x'"/\"(x'`"\/"y') & x'"/\"(x'`"\/"y') = x'"/\"x'`"\/"(x'
"/\"
y') & x'"/\"x'` = Bottom B &
Bottom B"\/"(x'"/\"y') = x'"/\"y' & x' [= (x'"/\"y')"\/"(x'"/\"a) & y'"/\"
x' [= y' &
y'"/\"x' = x'"/\"y' by LATTICES:23,27,39,47,def 11;
then x'"/\"a [= y' by LATTICES:25;
then (x'"/\"y')"\/"(x'"/\"a) [= y' by A26,FILTER_0:6;
then x' [= y' by A26,LATTICES:25;
hence [x,y] in R by Th32;
end;