filter_1.miz
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 ::
FILTER_1:1
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 ::
FILTER_1:2
<.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;
:: original:
/\
redefine
func F1
/\ F2 ->
Filter of L ;
coherence by
Th1;
end
definition
let D, R;
::
FILTER_1:def1
mode
UnOp of D,R ->
UnOp of D means
:
Def1: for x,y be
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;
::
FILTER_1:def2
mode
BinOp of D,R ->
BinOp of D means
:
Def2: for x1,y1,x2,y2 be
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;
::
FILTER_1:def3
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 be
object st x
in D & X
= (
Class (R,x)) by
EQREL_1:def 3;
hence X
<>
{} by
EQREL_1: 20;
end;
then
consider g be
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 be
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 be
Function of D, (
Class R) such that
A7: for x be
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 be
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 be
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;
::
FILTER_1:def4
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 be
object st x
in D & X
= (
Class (R,x)) by
EQREL_1:def 3;
hence X
<>
{} by
EQREL_1: 20;
end;
then
consider g be
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 be
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 be
Function of D, (
Class R) such that
A7: for x be
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 be
BinOp of (
Class R) such that
A8: for x,y be
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 be
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 be
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 be
object such that
A20: x1
in D and
A21: x
= (
Class (R,x1)) by
EQREL_1:def 3;
consider y1 be
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 ::
FILTER_1:3
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 ::
FILTER_1:sch1
SchAux1 { D() -> non
empty
set , R() ->
Equivalence_Relation of D() , P[
set] } :
for x be
Element of (
Class R()) holds P[x]
provided
A1: for x be
Element of D() holds P[(
EqClass (R(),x))];
let x be
Element of (
Class R());
ex y be
object st y
in D() & x
= (
Class (R(),y)) by
EQREL_1:def 3;
hence thesis by
A1;
end;
scheme ::
FILTER_1:sch2
SchAux2 { D() -> non
empty
set , R() ->
Equivalence_Relation of D() , P[
set,
set] } :
for x,y be
Element of (
Class R()) holds P[x, y]
provided
A1: for x,y be
Element of D() holds P[(
EqClass (R(),x)), (
EqClass (R(),y))];
let x1,x2 be
Element of (
Class R());
A2: ex y2 be
object st y2
in D() & x2
= (
Class (R(),y2)) by
EQREL_1:def 3;
ex y1 be
object st y1
in D() & x1
= (
Class (R(),y1)) by
EQREL_1:def 3;
hence thesis by
A1,
A2;
end;
scheme ::
FILTER_1:sch3
SchAux3 { D() -> non
empty
set , R() ->
Equivalence_Relation of D() , P[
set,
set,
set] } :
for x,y,z be
Element of (
Class R()) holds P[x, y, z]
provided
A1: for x,y,z be
Element of D() holds P[(
EqClass (R(),x)), (
EqClass (R(),y)), (
EqClass (R(),z))];
let x1,x2,x3 be
Element of (
Class R());
A2: ex y2 be
object st y2
in D() & x2
= (
Class (R(),y2)) by
EQREL_1:def 3;
A3: ex y3 be
object st y3
in D() & x3
= (
Class (R(),y3)) by
EQREL_1:def 3;
ex y1 be
object st y1
in D() & x1
= (
Class (R(),y1)) by
EQREL_1:def 3;
hence thesis by
A1,
A2,
A3;
end;
theorem ::
FILTER_1:4
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 be
Element of (
Class RD) holds
P[c1, c2] from
SchAux2(
A2);
end;
theorem ::
FILTER_1:5
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 be
Element of (
Class RD) holds
P[c1, c2, c3] from
SchAux3(
A2);
end;
theorem ::
FILTER_1:6
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 be
Element of (
Class RD) holds
P[c] from
SchAux1(
A2);
end;
theorem ::
FILTER_1:7
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 be
Element of (
Class RD) holds
P[c] from
SchAux1(
A2);
end;
theorem ::
FILTER_1:8
d
is_a_unity_wrt F implies (
EqClass (RD,d))
is_a_unity_wrt (F
/\/ RD) by
Th6,
Th7;
theorem ::
FILTER_1:9
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(.))) by
Th3
.=
Cl(.) by
Th3
.=
Cl(.) by
A1
.= ((G
/\/ RD)
. (
Cl(.),
Cl(.))) by
Th3
.= ((G
/\/ RD)
. (((F
/\/ RD)
. (
Cl(x1),
Cl(x2))),
Cl(.))) 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 be
Element of (
Class RD) holds
P[c1, c2, c3] from
SchAux3(
A2);
end;
theorem ::
FILTER_1:10
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(.),
Cl(x1))) by
Th3
.=
Cl(.) by
Th3
.=
Cl(.) by
A1
.= ((G
/\/ RD)
. (
Cl(.),
Cl(.))) by
Th3
.= ((G
/\/ RD)
. (((F
/\/ RD)
. (
Cl(x2),
Cl(x1))),
Cl(.))) 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 be
Element of (
Class RD) holds
P[c2, c3, c1] from
SchAux3(
A2);
end;
theorem ::
FILTER_1:11
F
is_distributive_wrt G implies (F
/\/ RD)
is_distributive_wrt (G
/\/ RD) by
Th9,
Th10;
theorem ::
FILTER_1:12
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 be
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(.))) by
Th3
.=
Cl(.) by
Th3
.=
Cl(x1) by
A1;
hence
P[(
EqClass (RD,x1)), (
EqClass (RD,x2))];
end;
thus for x,y be
Element of (
Class RD) holds
P[x, y] from
SchAux2(
A2);
end;
theorem ::
FILTER_1:13
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 ::
FILTER_1:14
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;
::
FILTER_1:def5
func L
/\/ F ->
strict
Lattice means
:
Def5: for R be
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 be
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 be
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;
::
FILTER_1:def6
func a
/\/ F ->
Element of (L
/\/ F) means
:
Def6: for R be
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 be
Equivalence_Relation of the
carrier of L st R
= (
equivalence_wrt F) holds c1
= (
Class (R,a)) and
A3: for R be
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 ::
FILTER_1:15
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 ::
FILTER_1:16
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 ::
FILTER_1:17
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 ::
FILTER_1:18
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 ::
FILTER_1:19
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 ::
FILTER_1:20
(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 be
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;
:: original:
|:
redefine
func
|:f1,f2:| ->
BinOp of
[:D1, D2:] ;
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 ::
FILTER_1:21
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 ::
FILTER_1:sch4
AuxCart1 { D1() -> non
empty
set , D2() -> non
empty
set , P[
set] } :
for d be
Element of
[:D1(), D2():] holds P[d]
provided
A1: for d1 be
Element of D1(), d2 be
Element of D2() holds P[
[d1, d2]];
let d be
Element of
[:D1(), D2():];
ex d1 be
Element of D1(), d2 be
Element of D2() st d
=
[d1, d2] by
DOMAIN_1: 1;
hence thesis by
A1;
end;
scheme ::
FILTER_1:sch5
AuxCart2 { D1() -> non
empty
set , D2() -> non
empty
set , P[
set,
set] } :
for d,d9 be
Element of
[:D1(), D2():] holds P[d, d9]
provided
A1: for d1,d19 be
Element of D1(), d2,d29 be
Element of D2() holds P[
[d1, d2],
[d19, d29]];
let d,d9 be
Element of
[:D1(), D2():];
A2: ex d19 be
Element of D1(), d29 be
Element of D2() st d9
=
[d19, d29] by
DOMAIN_1: 1;
ex d1 be
Element of D1(), d2 be
Element of D2() st d
=
[d1, d2] by
DOMAIN_1: 1;
hence thesis by
A1,
A2;
end;
scheme ::
FILTER_1:sch6
AuxCart3 { D1() -> non
empty
set , D2() -> non
empty
set , P[
set,
set,
set] } :
for a,b,c be
Element of
[:D1(), D2():] holds P[a, b, c]
provided
A1: for a1,b1,c1 be
Element of D1(), a2,b2,c2 be
Element of D2() holds P[
[a1, a2],
[b1, b2],
[c1, c2]];
let a,b,c be
Element of
[:D1(), D2():];
A2: ex b1 be
Element of D1(), b2 be
Element of D2() st b
=
[b1, b2] by
DOMAIN_1: 1;
A3: ex c1 be
Element of D1(), c2 be
Element of D2() st c
=
[c1, c2] by
DOMAIN_1: 1;
ex a1 be
Element of D1(), a2 be
Element of D2() st a
=
[a1, a2] by
DOMAIN_1: 1;
hence thesis by
A1,
A2,
A3;
end;
theorem ::
FILTER_1:22
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 be
Element of D1 holds (f1
. (a,b))
= (f1
. (b,a));
assume
A2: for a,b be
Element of D2 holds (f2
. (a,b))
= (f2
. (b,a));
A3: for d1,d19 be
Element of D1, d2,d29 be
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 be
Element of
[:D1, D2:] holds
P[a, b] from
AuxCart2(
A3);
end;
assume
A4: for a,b be
Element of
[:D1, D2:] holds (
|:f1, f2:|
. (a,b))
= (
|:f1, f2:|
. (b,a));
thus for a,b be
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 ::
FILTER_1:23
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 be
Element of D1 holds (f1
. (a,(f1
. (b,c))))
= (f1
. ((f1
. (a,b)),c));
assume
A2: for a,b,c be
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 be
Element of
[:D1, D2:] holds
P[a, b, c] from
AuxCart3(
A3);
end;
assume
A4: for a,b,c be
Element of
[:D1, D2:] holds (
|:f1, f2:|
. (a,(
|:f1, f2:|
. (b,c))))
= (
|:f1, f2:|
. ((
|:f1, f2:|
. (a,b)),c));
thus for a,b,c be
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 ::
FILTER_1:24
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 be
Element of
[:D1, D2:] holds
P[a] from
AuxCart1(
A3);
end;
assume
A4: for a be
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 ::
FILTER_1:25
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 be
Element of
[:D1, D2:] holds
P[a] from
AuxCart1(
A3);
end;
assume
A4: for a be
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 ::
FILTER_1:26
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 ::
FILTER_1:27
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 be
Element of
[:D1, D2:] holds
P[a, b, c] from
AuxCart3(
A3);
end;
assume
A4: for a,b,c be
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 ::
FILTER_1:28
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 be
Element of
[:D1, D2:] holds
P[a, b, c] from
AuxCart3(
A3);
then for b,c,a be
Element of
[:D1, D2:] holds
P[a, b, c];
hence thesis;
end;
assume
A4: for b,c,a be
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 ::
FILTER_1:29
Th29: f1
is_distributive_wrt g1 & f2
is_distributive_wrt g2 iff
|:f1, f2:|
is_distributive_wrt
|:g1, g2:| by
Th27,
Th28;
theorem ::
FILTER_1:30
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 be
Element of D1, d2,d29 be
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 be
Element of
[:D1, D2:] holds
P[a, b] from
AuxCart2(
A3);
end;
assume
A4: for a,b be
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;
::
FILTER_1:def7
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;
::
FILTER_1:def8
func
LattRel L ->
Relation equals {
[p, q] where p be
Element of L, q be
Element of L : p
[= q };
coherence
proof
now
let x be
object;
assume x
in {
[p, q] where p be
Element of L, q be
Element of L : p
[= q };
then ex p,q be
Element of L st x
=
[p, q] & p
[= q;
hence ex x1,x2 be
object st x
=
[x1, x2];
end;
hence thesis by
RELAT_1:def 1;
end;
end
theorem ::
FILTER_1:31
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 ::
FILTER_1:32
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 be
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 be
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 be
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 be
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;
::
FILTER_1:def9
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 ::
FILTER_1:33
for L1,L2,L3 be
Lattice st (L1,L2)
are_isomorphic & (L2,L3)
are_isomorphic holds (L1,L3)
are_isomorphic by
WELLORD1: 42;
theorem ::
FILTER_1:34
for L1,L2 be 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;
:: original:
[
redefine
func
[a,b] ->
Element of
[:L1, L2:] ;
coherence
proof
[a, b] is
Element of
[:the
carrier of L1, the
carrier of L2:];
hence thesis;
end;
end
theorem ::
FILTER_1:35
(
[p1, p2]
"\/"
[q1, q2])
=
[(p1
"\/" q1), (p2
"\/" q2)] & (
[p1, p2]
"/\"
[q1, q2])
=
[(p1
"/\" q1), (p2
"/\" q2)] by
Th21;
theorem ::
FILTER_1:36
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 ::
FILTER_1:37
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 ::
FILTER_1:38
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([:)
is_distributive_wrt
meet([:) 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 ::
FILTER_1:39
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 be
Element of
[:L1, L2:] such that
A4: for b be
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 ::
FILTER_1:40
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 be
Element of
[:L1, L2:] such that
A4: for b be
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 ::
FILTER_1:41
Th41: L1 is
bounded & L2 is
bounded iff
[:L1, L2:] is
bounded by
Th39,
Th40;
theorem ::
FILTER_1:42
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 ::
FILTER_1:43
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 ::
FILTER_1:44
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 ::
FILTER_1:45
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 be
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 be
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 ::
FILTER_1:46
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 ::
FILTER_1:47
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 holds ex r1 st (p1
"/\" r1)
[= q1 & for s1 st (p1
"/\" s1)
[= q1 holds s1
[= r1;
assume
A2: for p2, q2 holds 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 be
Element of
[:L1, L2:] holds ex c be
Element of
[:L1, L2:] st (a
"/\" c)
[= b & for d be
Element of
[:L1, L2:] st (a
"/\" d)
[= b holds d
[= c;
thus for p1, q1 holds 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 be
Element of
[:L1, L2:] such that
A13: (
[p1, p2]
"/\" c)
[=
[q1, p2] and
A14: for d be
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 be
Element of
[:L1, L2:] such that
A18: (
[p1, p2]
"/\" c)
[=
[p1, q2] and
A19: for d be
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 ::
FILTER_1:48
(
[:L1, L2:]
.: )
=
[:(L1
.: ), (L2
.: ):];
theorem ::
FILTER_1:49
(
[: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 be
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 ::
FILTER_1:50
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 ::
FILTER_1:51
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 ::
FILTER_1:52
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,
LATTICES: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,
LATTICES: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,
LATTICES: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,
LATTICES:def 5,
LATTICES:def 7,
LATTICES: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,
LATTICES: 9;
A21: (c
"/\" (
Top B))
[= (c
"/\" (c
=> b)) by
A19,
LATTICES: 6,
LATTICES: 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 ::
FILTER_1:53
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 ::
FILTER_1:54
((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,
LATTICES: 9;
A3: (j
"/\" ((i
"\/" j)
=> i))
[= ((i
"\/" j)
"/\" ((i
"\/" j)
=> i)) by
LATTICES: 5,
LATTICES: 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 ::
FILTER_1:55
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,
LATTICES: 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 ::
FILTER_1:56
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 ::
FILTER_1:57
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 ::
FILTER_1:58
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 ::
FILTER_1:59
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 ::
FILTER_1:60
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 ::
FILTER_1:61
(B,
[:(B
/\/
<.a.)), (
latt
<.a.)):])
are_isomorphic
proof
set F =
<.a.);
set E = (
equivalence_wrt F);
deffunc
F(
object) = (
Class (E,$1));
consider g be
Function such that
A1: (
dom g)
= the
carrier of B & for x be
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 be
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 be
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 be
Element of (
Class E), z be
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;