:: FILTER_1 semantic presentation
begin
deffunc H1( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
theorem Th1: :: FILTER_1:1
for L being Lattice
for F1, F2 being Filter of L holds F1 /\ F2 is Filter of L
proof
let L be Lattice; ::_thesis: for F1, F2 being Filter of L holds F1 /\ F2 is Filter of L
let F1, F2 be Filter of L; ::_thesis: F1 /\ F2 is Filter of L
consider p being Element of L such that
A1: p in F1 by SUBSET_1:4;
consider q being Element of L 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__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_F1_/\_F2_&_q_in_F1_/\_F2_)_iff_p_"/\"_q_in_F1_/\_F2_)
let p, q be Element of L; ::_thesis: ( ( p in F1 /\ F2 & q in F1 /\ F2 ) iff p "/\" q in F1 /\ F2 )
( 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; ::_thesis: verum
end;
then D is Filter of L by FILTER_0:8;
hence F1 /\ F2 is Filter of L ; ::_thesis: verum
end;
theorem :: FILTER_1:2
for L being Lattice
for p, q being Element of L st <.p.) = <.q.) holds
p = q
proof
let L be Lattice; ::_thesis: for p, q being Element of L st <.p.) = <.q.) holds
p = q
let p, q be Element of L; ::_thesis: ( <.p.) = <.q.) implies p = q )
assume A1: <.p.) = <.q.) ; ::_thesis: 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 p = q by A2, LATTICES:8; ::_thesis: verum
end;
definition
let L be Lattice;
let F1, F2 be Filter of L;
:: original: /\
redefine funcF1 /\ F2 -> Filter of L;
coherence
F1 /\ F2 is Filter of L by Th1;
end;
definition
let D be non empty set ;
let R be Relation;
mode UnOp of D,R -> UnOp of D means :Def1: :: FILTER_1:def 1
for x, y being Element of D st [x,y] in R holds
[(it . x),(it . y)] in R;
existence
ex b1 being UnOp of D st
for x, y being Element of D st [x,y] in R holds
[(b1 . x),(b1 . y)] in R
proof
reconsider f = id D as UnOp of D ;
take f ; ::_thesis: for x, y being Element of D st [x,y] in R holds
[(f . x),(f . y)] in R
let x, y be Element of D; ::_thesis: ( [x,y] in R implies [(f . x),(f . y)] in R )
f . x = x by FUNCT_1:18;
hence ( [x,y] in R implies [(f . x),(f . y)] in R ) by FUNCT_1:18; ::_thesis: verum
end;
mode BinOp of D,R -> BinOp of D means :Def2: :: FILTER_1:def 2
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
ex b1 being BinOp of D st
for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b1 . (x1,x2)),(b1 . (y1,y2))] in R
proof
take f = pr1 (D,D); ::_thesis: for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(f . (x1,x2)),(f . (y1,y2))] in R
let x1, y1, x2, y2 be Element of D; ::_thesis: ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R )
f . (x1,x2) = x1 by FUNCT_3:def_4;
hence ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R ) by FUNCT_3:def_4; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines UnOp FILTER_1:def_1_:_
for D being non empty set
for R being Relation
for b3 being UnOp of D holds
( b3 is UnOp of D,R iff for x, y being Element of D st [x,y] in R holds
[(b3 . x),(b3 . y)] in R );
:: deftheorem Def2 defines BinOp FILTER_1:def_2_:_
for D being non empty set
for R being Relation
for b3 being BinOp of D holds
( b3 is BinOp of D,R iff for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b3 . (x1,x2)),(b3 . (y1,y2))] in R );
definition
let D be non empty set ;
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 be non empty set ;
let R be Equivalence_Relation of D;
let u be UnOp of D;
assume A1: u is UnOp of D,R ;
funcu /\/ R -> UnOp of (Class R) means :: FILTER_1:def 3
for x, y being set st x in Class R & y in x holds
it . x = Class (R,(u . y));
existence
ex b1 being UnOp of (Class R) st
for x, y being set st x in Class R & y in x holds
b1 . x = Class (R,(u . y))
proof
now__::_thesis:_for_X_being_set_st_X_in_Class_R_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in Class R implies X <> {} )
assume X in Class R ; ::_thesis: X <> {}
then ex x being set st
( x in D & X = Class (R,x) ) by EQREL_1:def_3;
hence X <> {} by EQREL_1:20; ::_thesis: verum
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X being set st X in Class R holds
g . X in X by FUNCT_1:111;
A4: rng g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in D )
assume x in rng g ; ::_thesis: x in D
then consider y being set such that
A5: y in dom g and
A6: x = g . y by FUNCT_1:def_3;
x in y by A2, A3, A5, A6;
hence x in D by A2, A5; ::_thesis: verum
end;
deffunc H3( Element of D) -> Element of Class R = EqClass (R,$1);
consider f being Function of D,(Class R) such that
A7: for x being Element of D holds f . x = H3(x) from FUNCT_2:sch_4();
reconsider g = g as Function of (Class R),D by A2, A4, FUNCT_2:def_1, RELSET_1:4;
take uR = (f * u) * g; ::_thesis: for x, y being set st x in Class R & y in x holds
uR . x = Class (R,(u . y))
let x, y be set ; ::_thesis: ( x in Class R & y in x implies uR . x = Class (R,(u . y)) )
assume that
A8: x in Class R and
A9: y in x ; ::_thesis: uR . x = Class (R,(u . y))
A10: D = dom (f * u) by FUNCT_2:def_1;
g . x in rng g by A2, A8, FUNCT_1:def_3;
then A11: (f * u) . (g . x) = f . (u . (g . x)) by A4, A10, FUNCT_1:12;
Class R = dom uR by FUNCT_2:def_1;
then A12: uR . x = (f * u) . (g . x) by A8, FUNCT_1:12;
reconsider x9 = x as Element of Class R by A8;
reconsider y9 = y as Element of D by A8, A9;
A13: ex x1 being set 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 uR . x = Class (R,(u . y)) by A12, A11, A14, EQREL_1:23; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOp of (Class R) st ( for x, y being set st x in Class R & y in x holds
b1 . x = Class (R,(u . y)) ) & ( for x, y being set st x in Class R & y in x holds
b2 . x = Class (R,(u . y)) ) holds
b1 = b2
proof
let u1, u2 be UnOp of (Class R); ::_thesis: ( ( for x, y being set st x in Class R & y in x holds
u1 . x = Class (R,(u . y)) ) & ( for x, y being set st x in Class R & y in x holds
u2 . x = Class (R,(u . y)) ) implies u1 = u2 )
assume that
A15: for x, y being set st x in Class R & y in x holds
u1 . x = Class (R,(u . y)) and
A16: for x, y being set st x in Class R & y in x holds
u2 . x = Class (R,(u . y)) ; ::_thesis: u1 = u2
now__::_thesis:_for_x_being_set_st_x_in_Class_R_holds_
u1_._x_=_u2_._x
let x be set ; ::_thesis: ( x in Class R implies u1 . x = u2 . x )
assume A17: x in Class R ; ::_thesis: u1 . x = u2 . x
then consider y being set 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; ::_thesis: verum
end;
hence u1 = u2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem defines /\/ FILTER_1:def_3_:_
for D being non empty set
for R being Equivalence_Relation of D
for u being UnOp of D st u is UnOp of D,R holds
for b4 being UnOp of (Class R) holds
( b4 = u /\/ R iff for x, y being set st x in Class R & y in x holds
b4 . x = Class (R,(u . y)) );
definition
let D be non empty set ;
let R be Equivalence_Relation of D;
let b be BinOp of D;
assume A1: b is BinOp of D,R ;
funcb /\/ R -> BinOp of (Class R) means :Def4: :: FILTER_1:def 4
for x, y, x1, y1 being set 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
ex b1 being BinOp of (Class R) st
for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1)))
proof
now__::_thesis:_for_X_being_set_st_X_in_Class_R_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in Class R implies X <> {} )
assume X in Class R ; ::_thesis: X <> {}
then ex x being set st
( x in D & X = Class (R,x) ) by EQREL_1:def_3;
hence X <> {} by EQREL_1:20; ::_thesis: verum
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X being set st X in Class R holds
g . X in X by FUNCT_1:111;
A4: rng g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in D )
assume x in rng g ; ::_thesis: x in D
then consider y being set such that
A5: y in dom g and
A6: x = g . y by FUNCT_1:def_3;
x in y by A2, A3, A5, A6;
hence x in D by A2, A5; ::_thesis: verum
end;
deffunc H3( Element of D) -> Element of Class R = EqClass (R,$1);
consider f being Function of D,(Class R) such that
A7: for x being Element of D holds f . x = H3(x) from FUNCT_2:sch_4();
reconsider g = g as Function of (Class R),D by A2, A4, FUNCT_2:def_1, RELSET_1:4;
deffunc H4( Element of Class R, Element of Class R) -> Element of Class R = f . (b . ((g . $1),(g . $2)));
consider bR being BinOp of (Class R) such that
A8: for x, y being Element of Class R holds bR . (x,y) = H4(x,y) from BINOP_1:sch_4();
take bR ; ::_thesis: for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
bR . (x,y) = Class (R,(b . (x1,y1)))
let x, y, x1, y1 be set ; ::_thesis: ( x in Class R & y in Class R & x1 in x & y1 in y implies bR . (x,y) = Class (R,(b . (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 ; ::_thesis: bR . (x,y) = Class (R,(b . (x1,y1)))
reconsider x9 = x, y9 = y as Element of Class R by A9, A10;
reconsider x19 = x1, y19 = y1 as Element of D by A9, A10, A11, A12;
A13: ex y2 being set st
( y2 in D & y9 = Class (R,y2) ) by EQREL_1:def_3;
g . y9 in y by A3;
then A14: [(g . y9),y19] in R by A12, A13, EQREL_1:22;
A15: ex x2 being set 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 bR . (x,y) = Class (R,(b . (x1,y1))) by A16, A17, EQREL_1:23; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Class R) st ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1))) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ) holds
b1 = b2
proof
let b1, b2 be BinOp of (Class R); ::_thesis: ( ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1))) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ) implies b1 = b2 )
assume that
A18: for x, y, x1, y1 being set 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 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ; ::_thesis: b1 = b2
now__::_thesis:_for_x,_y_being_Element_of_Class_R_holds_b1_._(x,y)_=_b2_._(x,y)
let x, y be Element of Class R; ::_thesis: b1 . (x,y) = b2 . (x,y)
consider x1 being set such that
A20: x1 in D and
A21: x = Class (R,x1) by EQREL_1:def_3;
consider y1 being set 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; ::_thesis: verum
end;
hence b1 = b2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines /\/ FILTER_1:def_4_:_
for D being non empty set
for R being Equivalence_Relation of D
for b being BinOp of D st b is BinOp of D,R holds
for b4 being BinOp of (Class R) holds
( b4 = b /\/ R iff for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b4 . (x,y) = Class (R,(b . (x1,y1))) );
theorem Th3: :: FILTER_1:3
for D being non empty set
for RD being Equivalence_Relation of D
for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let RD be Equivalence_Relation of D; ::_thesis: for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let a, b be Element of D; ::_thesis: for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let F be BinOp of D,RD; ::_thesis: (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
A1: b in EqClass (RD,b) by EQREL_1:20;
a in EqClass (RD,a) by EQREL_1:20;
hence (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b))) by A1, Def4; ::_thesis: verum
end;
scheme :: FILTER_1:sch 1
SchAux1{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set ] } :
for x being Element of Class F2() holds P1[x]
provided
A1: for x being Element of F1() holds P1[ EqClass (F2(),x)]
proof
let x be Element of Class F2(); ::_thesis: P1[x]
ex y being set st
( y in F1() & x = Class (F2(),y) ) by EQREL_1:def_3;
hence P1[x] by A1; ::_thesis: verum
end;
scheme :: FILTER_1:sch 2
SchAux2{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set , set ] } :
for x, y being Element of Class F2() holds P1[x,y]
provided
A1: for x, y being Element of F1() holds P1[ EqClass (F2(),x), EqClass (F2(),y)]
proof
let x1, x2 be Element of Class F2(); ::_thesis: P1[x1,x2]
A2: ex y2 being set st
( y2 in F1() & x2 = Class (F2(),y2) ) by EQREL_1:def_3;
ex y1 being set st
( y1 in F1() & x1 = Class (F2(),y1) ) by EQREL_1:def_3;
hence P1[x1,x2] by A1, A2; ::_thesis: verum
end;
scheme :: FILTER_1:sch 3
SchAux3{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set , set , set ] } :
for x, y, z being Element of Class F2() holds P1[x,y,z]
provided
A1: for x, y, z being Element of F1() holds P1[ EqClass (F2(),x), EqClass (F2(),y), EqClass (F2(),z)]
proof
let x1, x2, x3 be Element of Class F2(); ::_thesis: P1[x1,x2,x3]
A2: ex y2 being set st
( y2 in F1() & x2 = Class (F2(),y2) ) by EQREL_1:def_3;
A3: ex y3 being set st
( y3 in F1() & x3 = Class (F2(),y3) ) by EQREL_1:def_3;
ex y1 being set st
( y1 in F1() & x1 = Class (F2(),y1) ) by EQREL_1:def_3;
hence P1[x1,x2,x3] by A1, A2, A3; ::_thesis: verum
end;
theorem Th4: :: FILTER_1:4
for D being non empty set
for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
let RD be Equivalence_Relation of D; ::_thesis: for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
let F be BinOp of D,RD; ::_thesis: ( F is commutative implies F /\/ RD is commutative )
defpred S1[ Element of Class RD, Element of Class RD] means (F /\/ RD) . ($1,$2) = (F /\/ RD) . ($2,$1);
assume A1: for a, b being Element of D holds F . (a,b) = F . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: F /\/ RD is commutative
A2: now__::_thesis:_for_x1,_x2_being_Element_of_D_holds_S1[_EqClass_(RD,x1),_EqClass_(RD,x2)]
let x1, x2 be Element of D; ::_thesis: S1[ EqClass (RD,x1), EqClass (RD,x2)]
(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 S1[ EqClass (RD,x1), EqClass (RD,x2)] ; ::_thesis: verum
end;
thus for c1, c2 being Element of Class RD holds S1[c1,c2] from FILTER_1:sch_2(A2); :: according to BINOP_1:def_2 ::_thesis: verum
end;
theorem Th5: :: FILTER_1:5
for D being non empty set
for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is associative holds
F /\/ RD is associative
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is associative holds
F /\/ RD is associative
let RD be Equivalence_Relation of D; ::_thesis: for F being BinOp of D,RD st F is associative holds
F /\/ RD is associative
let F be BinOp of D,RD; ::_thesis: ( F is associative implies F /\/ RD is associative )
defpred S1[ 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 being Element of D holds F . (d,(F . (a,b))) = F . ((F . (d,a)),b) ; :: according to BINOP_1:def_3 ::_thesis: F /\/ RD is associative
A2: now__::_thesis:_for_x1,_x2,_x3_being_Element_of_D_holds_S1[_EqClass_(RD,x1),_EqClass_(RD,x2),_EqClass_(RD,x3)]
let x1, x2, x3 be Element of D; ::_thesis: S1[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)]
(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 S1[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)] ; ::_thesis: verum
end;
thus for c1, c2, c3 being Element of Class RD holds S1[c1,c2,c3] from FILTER_1:sch_3(A2); :: according to BINOP_1:def_3 ::_thesis: verum
end;
theorem Th6: :: FILTER_1:6
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_left_unity_wrt F holds
EqClass (RD,d) is_a_left_unity_wrt F /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_left_unity_wrt F holds
EqClass (RD,d) is_a_left_unity_wrt F /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for d being Element of D
for F being BinOp of D,RD st d is_a_left_unity_wrt F holds
EqClass (RD,d) is_a_left_unity_wrt F /\/ RD
let d be Element of D; ::_thesis: for F being BinOp of D,RD st d is_a_left_unity_wrt F holds
EqClass (RD,d) is_a_left_unity_wrt F /\/ RD
let F be BinOp of D,RD; ::_thesis: ( d is_a_left_unity_wrt F implies EqClass (RD,d) is_a_left_unity_wrt F /\/ RD )
defpred S1[ Element of Class RD] means (F /\/ RD) . ((EqClass (RD,d)),$1) = $1;
assume A1: for a being Element of D holds F . (d,a) = a ; :: according to BINOP_1:def_16 ::_thesis: EqClass (RD,d) is_a_left_unity_wrt F /\/ RD
A2: now__::_thesis:_for_a_being_Element_of_D_holds_S1[_EqClass_(RD,a)]
let a be Element of D; ::_thesis: S1[ EqClass (RD,a)]
(F /\/ RD) . ((EqClass (RD,d)),(EqClass (RD,a))) = Class (RD,(F . (d,a))) by Th3
.= EqClass (RD,a) by A1 ;
hence S1[ EqClass (RD,a)] ; ::_thesis: verum
end;
thus for c being Element of Class RD holds S1[c] from FILTER_1:sch_1(A2); :: according to BINOP_1:def_16 ::_thesis: verum
end;
theorem Th7: :: FILTER_1:7
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for d being Element of D
for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
let d be Element of D; ::_thesis: for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
let F be BinOp of D,RD; ::_thesis: ( d is_a_right_unity_wrt F implies EqClass (RD,d) is_a_right_unity_wrt F /\/ RD )
defpred S1[ Element of Class RD] means (F /\/ RD) . ($1,(EqClass (RD,d))) = $1;
assume A1: for a being Element of D holds F . (a,d) = a ; :: according to BINOP_1:def_17 ::_thesis: EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
A2: now__::_thesis:_for_a_being_Element_of_D_holds_S1[_EqClass_(RD,a)]
let a be Element of D; ::_thesis: S1[ EqClass (RD,a)]
(F /\/ RD) . ((EqClass (RD,a)),(EqClass (RD,d))) = EqClass (RD,(F . (a,d))) by Th3
.= EqClass (RD,a) by A1 ;
hence S1[ EqClass (RD,a)] ; ::_thesis: verum
end;
thus for c being Element of Class RD holds S1[c] from FILTER_1:sch_1(A2); :: according to BINOP_1:def_17 ::_thesis: verum
end;
theorem :: FILTER_1:8
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let d be Element of D; ::_thesis: for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let F be BinOp of D,RD; ::_thesis: ( d is_a_unity_wrt F implies EqClass (RD,d) is_a_unity_wrt F /\/ RD )
assume that
A1: d is_a_left_unity_wrt F and
A2: d is_a_right_unity_wrt F ; :: according to BINOP_1:def_7 ::_thesis: EqClass (RD,d) is_a_unity_wrt F /\/ RD
thus ( EqClass (RD,d) is_a_left_unity_wrt F /\/ RD & EqClass (RD,d) is_a_right_unity_wrt F /\/ RD ) by A1, A2, Th6, Th7; :: according to BINOP_1:def_7 ::_thesis: verum
end;
theorem Th9: :: FILTER_1:9
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
let F, G be BinOp of D,RD; ::_thesis: ( F is_left_distributive_wrt G implies F /\/ RD is_left_distributive_wrt G /\/ RD )
deffunc H3( Element of D) -> Element of Class RD = EqClass (RD,$1);
defpred S1[ 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 being Element of D holds F . (d,(G . (a,b))) = G . ((F . (d,a)),(F . (d,b))) ; :: according to BINOP_1:def_18 ::_thesis: F /\/ RD is_left_distributive_wrt G /\/ RD
A2: now__::_thesis:_for_x1,_x2,_x3_being_Element_of_D_holds_S1[_EqClass_(RD,x1),_EqClass_(RD,x2),_EqClass_(RD,x3)]
let x1, x2, x3 be Element of D; ::_thesis: S1[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)]
(F /\/ RD) . (H3(x1),((G /\/ RD) . (H3(x2),H3(x3)))) = (F /\/ RD) . (H3(x1),H3(G . (x2,x3))) by Th3
.= H3(F . (x1,(G . (x2,x3)))) by Th3
.= H3(G . ((F . (x1,x2)),(F . (x1,x3)))) by A1
.= (G /\/ RD) . (H3(F . (x1,x2)),H3(F . (x1,x3))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x1),H3(x2))),H3(F . (x1,x3))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x1),H3(x2))),((F /\/ RD) . (H3(x1),H3(x3)))) by Th3 ;
hence S1[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)] ; ::_thesis: verum
end;
thus for c1, c2, c3 being Element of Class RD holds S1[c1,c2,c3] from FILTER_1:sch_3(A2); :: according to BINOP_1:def_18 ::_thesis: verum
end;
theorem Th10: :: FILTER_1:10
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds
F /\/ RD is_right_distributive_wrt G /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds
F /\/ RD is_right_distributive_wrt G /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds
F /\/ RD is_right_distributive_wrt G /\/ RD
let F, G be BinOp of D,RD; ::_thesis: ( F is_right_distributive_wrt G implies F /\/ RD is_right_distributive_wrt G /\/ RD )
deffunc H3( Element of D) -> Element of Class RD = EqClass (RD,$1);
defpred S1[ 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 being Element of D holds F . ((G . (a,b)),d) = G . ((F . (a,d)),(F . (b,d))) ; :: according to BINOP_1:def_19 ::_thesis: F /\/ RD is_right_distributive_wrt G /\/ RD
A2: now__::_thesis:_for_x2,_x3,_x1_being_Element_of_D_holds_S1[_EqClass_(RD,x2),_EqClass_(RD,x3),_EqClass_(RD,x1)]
let x2, x3, x1 be Element of D; ::_thesis: S1[ EqClass (RD,x2), EqClass (RD,x3), EqClass (RD,x1)]
(F /\/ RD) . (((G /\/ RD) . (H3(x2),H3(x3))),H3(x1)) = (F /\/ RD) . (H3(G . (x2,x3)),H3(x1)) by Th3
.= H3(F . ((G . (x2,x3)),x1)) by Th3
.= H3(G . ((F . (x2,x1)),(F . (x3,x1)))) by A1
.= (G /\/ RD) . (H3(F . (x2,x1)),H3(F . (x3,x1))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x2),H3(x1))),H3(F . (x3,x1))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x2),H3(x1))),((F /\/ RD) . (H3(x3),H3(x1)))) by Th3 ;
hence S1[ EqClass (RD,x2), EqClass (RD,x3), EqClass (RD,x1)] ; ::_thesis: verum
end;
thus for c2, c3, c1 being Element of Class RD holds S1[c2,c3,c1] from FILTER_1:sch_3(A2); :: according to BINOP_1:def_19 ::_thesis: verum
end;
theorem :: FILTER_1:11
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD
let F, G be BinOp of D,RD; ::_thesis: ( F is_distributive_wrt G implies F /\/ RD is_distributive_wrt G /\/ RD )
assume that
A1: F is_left_distributive_wrt G and
A2: F is_right_distributive_wrt G ; :: according to BINOP_1:def_11 ::_thesis: F /\/ RD is_distributive_wrt G /\/ RD
thus ( F /\/ RD is_left_distributive_wrt G /\/ RD & F /\/ RD is_right_distributive_wrt G /\/ RD ) by A1, A2, Th9, Th10; :: according to BINOP_1:def_11 ::_thesis: verum
end;
theorem Th12: :: FILTER_1:12
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
proof
let D be non empty set ; ::_thesis: for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
let RD be Equivalence_Relation of D; ::_thesis: for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
let F, G be BinOp of D,RD; ::_thesis: ( F absorbs G implies F /\/ RD absorbs G /\/ RD )
deffunc H3( Element of D) -> Element of Class RD = EqClass (RD,$1);
defpred S1[ Element of Class RD, Element of Class RD] means (F /\/ RD) . ($1,((G /\/ RD) . ($1,$2))) = $1;
assume A1: for x, y being Element of D holds F . (x,(G . (x,y))) = x ; :: according to LATTICE2:def_1 ::_thesis: F /\/ RD absorbs G /\/ RD
A2: now__::_thesis:_for_x1,_x2_being_Element_of_D_holds_S1[_EqClass_(RD,x1),_EqClass_(RD,x2)]
let x1, x2 be Element of D; ::_thesis: S1[ EqClass (RD,x1), EqClass (RD,x2)]
(F /\/ RD) . (H3(x1),((G /\/ RD) . (H3(x1),H3(x2)))) = (F /\/ RD) . (H3(x1),H3(G . (x1,x2))) by Th3
.= H3(F . (x1,(G . (x1,x2)))) by Th3
.= H3(x1) by A1 ;
hence S1[ EqClass (RD,x1), EqClass (RD,x2)] ; ::_thesis: verum
end;
thus for x, y being Element of Class RD holds S1[x,y] from FILTER_1:sch_2(A2); :: according to LATTICE2:def_1 ::_thesis: verum
end;
theorem Th13: :: FILTER_1:13
for I being I_Lattice
for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
let FI be Filter of I; ::_thesis: the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
set R = equivalence_wrt FI;
let x1, y1, x2, y2 be Element of the carrier of I; :: according to FILTER_1:def_2 ::_thesis: ( [x1,y1] in equivalence_wrt FI & [x2,y2] in equivalence_wrt FI implies [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI )
assume that
A1: [x1,y1] in equivalence_wrt FI and
A2: [x2,y2] in equivalence_wrt FI ; ::_thesis: [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI
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 [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI by FILTER_0:def_11; ::_thesis: verum
end;
theorem Th14: :: FILTER_1:14
for I being I_Lattice
for FI being Filter of I holds the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I holds the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI
let FI be Filter of I; ::_thesis: the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI
set R = equivalence_wrt FI;
let x1, y1, x2, y2 be Element of I; :: according to FILTER_1:def_2 ::_thesis: ( [x1,y1] in equivalence_wrt FI & [x2,y2] in equivalence_wrt FI implies [( the L_meet of I . (x1,x2)),( the L_meet of I . (y1,y2))] in equivalence_wrt FI )
assume that
A1: [x1,y1] in equivalence_wrt FI and
A2: [x2,y2] in equivalence_wrt FI ; ::_thesis: [( the L_meet of I . (x1,x2)),( the L_meet of I . (y1,y2))] in equivalence_wrt FI
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 [( the L_meet of I . (x1,x2)),( the L_meet of I . (y1,y2))] in equivalence_wrt FI by FILTER_0:def_11; ::_thesis: verum
end;
definition
let L be Lattice;
let F be Filter of L;
assume A1: L is I_Lattice ;
funcL /\/ F -> strict Lattice means :Def5: :: FILTER_1:def 5
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
ex b1 being strict Lattice st
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #)
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: H1(LL) is commutative by Th4;
A3: H1(LL) is associative by Th5;
A4: H2(LL) is associative by Th5;
A5: H2(LL) is commutative by Th4;
A6: H2(LL) absorbs H1(LL) by Th12, LATTICE2:27;
H1(LL) absorbs H2(LL) by Th12, LATTICE2:26;
then reconsider LL = LL as strict Lattice by A2, A3, A5, A4, A6, LATTICE2:11;
take LL ; ::_thesis: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #)
thus for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Lattice st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b2 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) holds
b1 = b2
proof
reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I ;
set R = equivalence_wrt FI;
reconsider o1 = H1(L), o2 = H2(L) as BinOp of equivalence_wrt FI by Th13, Th14;
let L1, L2 be strict Lattice; ::_thesis: ( ( 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) #) ) & ( 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) #) ) implies L1 = L2 )
assume that
A7: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
L1 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) and
A8: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
L2 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ; ::_thesis: L1 = L2
thus L1 = LattStr(# (Class (equivalence_wrt FI)),(o1 /\/ (equivalence_wrt FI)),(o2 /\/ (equivalence_wrt FI)) #) by A7
.= L2 by A8 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines /\/ FILTER_1:def_5_:_
for L being Lattice
for F being Filter of L st L is I_Lattice holds
for b3 being strict Lattice holds
( b3 = L /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b3 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) );
definition
let L be Lattice;
let F be Filter of L;
let a be Element of L;
assume A1: L is I_Lattice ;
funca /\/ F -> Element of (L /\/ F) means :Def6: :: FILTER_1:def 6
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
it = Class (R,a);
existence
ex b1 being Element of (L /\/ F) st
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = Class (R,a)
proof
reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I ;
set R = equivalence_wrt FI;
reconsider j = H1(I), m = H2(I) as BinOp of equivalence_wrt FI by Th13, Th14;
reconsider i = a as Element of I ;
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(j /\/ (equivalence_wrt FI)),(m /\/ (equivalence_wrt FI)) #) by Def5;
then reconsider c = EqClass ((equivalence_wrt FI),i) as Element of (L /\/ F) ;
take c ; ::_thesis: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c = Class (R,a)
thus for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c = Class (R,a) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of (L /\/ F) st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = Class (R,a) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b2 = Class (R,a) ) holds
b1 = b2
proof
reconsider I = L as I_Lattice by A1;
let c1, c2 be Element of (L /\/ F); ::_thesis: ( ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c1 = Class (R,a) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c2 = Class (R,a) ) implies c1 = c2 )
assume 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) ; ::_thesis: c1 = c2
reconsider FI = F as Filter of I ;
c1 = Class ((equivalence_wrt FI),a) by A2;
hence c1 = c2 by A3; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines /\/ FILTER_1:def_6_:_
for L being Lattice
for F being Filter of L
for a being Element of L st L is I_Lattice holds
for b4 being Element of (L /\/ F) holds
( b4 = a /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b4 = Class (R,a) );
theorem Th15: :: FILTER_1:15
for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
let FI be Filter of I; ::_thesis: for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
let i, j be Element of I; ::_thesis: ( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
set R = equivalence_wrt FI;
A1: j /\/ FI = Class ((equivalence_wrt FI),j) by Def6;
reconsider jj = H1(I), mm = H2(I) as BinOp of equivalence_wrt FI by Th13, Th14;
A2: i /\/ FI = Class ((equivalence_wrt FI),i) by Def6;
A3: I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(jj /\/ (equivalence_wrt FI)),(mm /\/ (equivalence_wrt FI)) #) by Def5;
(i "\/" j) /\/ FI = Class ((equivalence_wrt FI),(i "\/" j)) by Def6;
hence (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI by A2, A1, A3, Th3; ::_thesis: (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI
(i "/\" j) /\/ FI = Class ((equivalence_wrt FI),(i "/\" j)) by Def6;
hence (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI by A2, A1, A3, Th3; ::_thesis: verum
end;
theorem Th16: :: FILTER_1:16
for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
let FI be Filter of I; ::_thesis: for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
let i, j be Element of I; ::_thesis: ( i /\/ FI [= j /\/ FI iff i => j in FI )
set R = equivalence_wrt FI;
set a = i "\/" j;
set b = (i "\/" j) => j;
A1: j "/\" (i => j) [= j by FILTER_0:2;
A2: j "\/" j = j ;
thus ( i /\/ FI [= j /\/ FI implies i => j in FI ) ::_thesis: ( i => j in FI implies i /\/ FI [= j /\/ FI )
proof
assume (i /\/ FI) "\/" (j /\/ FI) = j /\/ FI ; :: according to LATTICES:def_3 ::_thesis: i => j in FI
then A3: (i "\/" j) /\/ FI = j /\/ FI by Th15;
A4: i "\/" j in Class ((equivalence_wrt FI),(i "\/" j)) by EQREL_1:20;
A5: i "/\" ((i "\/" j) => j) [= (i "/\" ((i "\/" j) => j)) "\/" (j "/\" ((i "\/" j) => j)) by LATTICES:5;
A6: j /\/ FI = Class ((equivalence_wrt FI),j) by Def6;
A7: j in Class ((equivalence_wrt FI),j) by EQREL_1:20;
Class ((equivalence_wrt FI),(i "\/" j)) = (i "\/" j) /\/ FI by Def6;
then [(i "\/" j),j] in equivalence_wrt FI 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: (i "\/" j) "/\" ((i "\/" j) => j) [= j by FILTER_0:def_7;
(i "\/" j) "/\" ((i "\/" j) => j) = (i "/\" ((i "\/" j) => j)) "\/" (j "/\" ((i "\/" j) => j)) by LATTICES:def_11;
then i "/\" ((i "\/" j) => j) [= j by A9, A5, LATTICES:7;
then (i "\/" j) => j [= i => j by FILTER_0:def_7;
hence i => j in FI by A8, FILTER_0:9; ::_thesis: verum
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, FILTER_0:9;
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 ; ::_thesis: i /\/ FI [= j /\/ 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 equivalence_wrt FI by FILTER_0:def_11;
thus (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI by Th15
.= Class ((equivalence_wrt FI),(i "\/" j)) by Def6
.= Class ((equivalence_wrt FI),j) by A14, EQREL_1:35
.= j /\/ FI by Def6 ; :: according to LATTICES:def_3 ::_thesis: verum
end;
theorem Th17: :: FILTER_1:17
for I being I_Lattice
for i, j, k being Element of I holds (i "/\" j) => k = i => (j => k)
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I holds (i "/\" j) => k = i => (j => k)
let i, j, k be Element of I; ::_thesis: (i "/\" j) => k = i => (j => k)
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 (i "/\" j) => k = i => (j => k) by A2, LATTICES:8; ::_thesis: verum
end;
theorem Th18: :: FILTER_1:18
for I being I_Lattice
for FI being Filter of I st I is lower-bounded holds
( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I st I is lower-bounded holds
( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
let FI be Filter of I; ::_thesis: ( I is lower-bounded implies ( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI ) )
set L = I /\/ FI;
set R = equivalence_wrt FI;
assume A1: I is lower-bounded ; ::_thesis: ( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
then consider i being Element of I such that
A2: for j being Element of I holds
( i "/\" j = i & j "/\" i = i ) by LATTICES:def_13;
set x = i /\/ FI;
A3: now__::_thesis:_for_y_being_Element_of_(I_/\/_FI)_holds_
(_(i_/\/_FI)_"/\"_y_=_i_/\/_FI_&_y_"/\"_(i_/\/_FI)_=_i_/\/_FI_)
let y be Element of (I /\/ FI); ::_thesis: ( (i /\/ FI) "/\" y = i /\/ FI & y "/\" (i /\/ FI) = i /\/ FI )
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),( the L_join of I /\/ (equivalence_wrt FI)),( the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider j being Element of I such that
A4: y = Class ((equivalence_wrt FI),j) by EQREL_1:36;
A5: i "/\" j = i by A2;
A6: y = j /\/ FI by A4, Def6;
hence (i /\/ FI) "/\" y = i /\/ FI by A5, Th15; ::_thesis: y "/\" (i /\/ FI) = i /\/ FI
thus y "/\" (i /\/ FI) = i /\/ FI by A5, A6, Th15; ::_thesis: verum
end;
hence A7: I /\/ FI is 0_Lattice by LATTICES:def_13; ::_thesis: Bottom (I /\/ FI) = (Bottom I) /\/ FI
Bottom I = i by A1, A2, LATTICES:def_16;
hence Bottom (I /\/ FI) = (Bottom I) /\/ FI by A3, A7, LATTICES:def_16; ::_thesis: verum
end;
theorem Th19: :: FILTER_1:19
for I being I_Lattice
for FI being Filter of I holds
( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I holds
( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
let FI be Filter of I; ::_thesis: ( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
set L = I /\/ FI;
set R = equivalence_wrt FI;
set x = (Top I) /\/ FI;
A1: now__::_thesis:_for_y_being_Element_of_(I_/\/_FI)_holds_
(_((Top_I)_/\/_FI)_"\/"_y_=_(Top_I)_/\/_FI_&_y_"\/"_((Top_I)_/\/_FI)_=_(Top_I)_/\/_FI_)
let y be Element of (I /\/ FI); ::_thesis: ( ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI & y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI )
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),( the L_join of I /\/ (equivalence_wrt FI)),( the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider j being Element of I such that
A2: y = Class ((equivalence_wrt FI),j) by EQREL_1:36;
A3: (Top I) "\/" j = Top I ;
A4: y = j /\/ FI by A2, Def6;
hence ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI by A3, Th15; ::_thesis: y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI
thus y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI by A3, A4, Th15; ::_thesis: verum
end;
hence I /\/ FI is 1_Lattice by LATTICES:def_14; ::_thesis: Top (I /\/ FI) = (Top I) /\/ FI
hence Top (I /\/ FI) = (Top I) /\/ FI by A1, LATTICES:def_17; ::_thesis: verum
end;
registration
let I be I_Lattice;
let FI be Filter of I;
clusterI /\/ FI -> strict implicative ;
coherence
I /\/ FI is implicative
proof
set L = I /\/ FI;
set R = equivalence_wrt FI;
let x, y be Element of (I /\/ FI); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (I /\/ FI) st
( x "/\" b1 [= y & ( for b2 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b2 [= y or b2 [= b1 ) ) )
A1: Top I in FI by FILTER_0:11;
A2: I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),( the L_join of I /\/ (equivalence_wrt FI)),( the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider i being Element of I such that
A3: x = Class ((equivalence_wrt FI),i) by EQREL_1:36;
A4: x = i /\/ FI by A3, Def6;
consider j being Element of I such that
A5: y = Class ((equivalence_wrt FI),j) by A2, EQREL_1:36;
A6: y = j /\/ FI by A5, Def6;
take z = (i => j) /\/ FI; ::_thesis: ( x "/\" z [= y & ( for b1 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b1 [= y or b1 [= z ) ) )
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, FILTER_0:9;
then (i "/\" (i => j)) /\/ FI [= y by A6, Th16;
hence x "/\" z [= y by A4, Th15; ::_thesis: for b1 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b1 [= y or b1 [= z )
let t be Element of (I /\/ FI); ::_thesis: ( not x "/\" t [= y or t [= z )
consider k being Element of I such that
A8: t = Class ((equivalence_wrt FI),k) by A2, EQREL_1:36;
A9: k /\/ FI = t by A8, Def6;
assume A10: x "/\" t [= y ; ::_thesis: t [= z
(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 t [= z by A9, Th16; ::_thesis: verum
end;
end;
theorem :: FILTER_1:20
for B being B_Lattice
for FB being Filter of B holds B /\/ FB is B_Lattice
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B holds B /\/ FB is B_Lattice
let FB be Filter of B; ::_thesis: B /\/ FB is B_Lattice
set L = B /\/ FB;
set R = equivalence_wrt FB;
A1: B /\/ FB is 0_Lattice by Th18;
A2: Bottom (B /\/ FB) = (Bottom B) /\/ FB by Th18;
A3: Top (B /\/ FB) = (Top B) /\/ FB by Th19;
reconsider L = B /\/ FB as 01_Lattice by A1;
A4: L is complemented
proof
let x be Element of L; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of x
L = LattStr(# (Class (equivalence_wrt FB)),( the L_join of B /\/ (equivalence_wrt FB)),( the L_meet of B /\/ (equivalence_wrt FB)) #) by Def5;
then consider a being Element of B such that
A5: x = Class ((equivalence_wrt FB),a) by EQREL_1:36;
reconsider y = (a `) /\/ FB as Element of L ;
take y ; ::_thesis: y is_a_complement_of x
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 ;
:: according to LATTICES:def_18 ::_thesis: ( x "\/" y = Top L & y "/\" x = Bottom L & x "/\" y = Bottom L )
hence x "\/" y = Top L ; ::_thesis: ( y "/\" x = Bottom L & x "/\" y = Bottom L )
thus y "/\" x = ((a `) "/\" a) /\/ FB by A6, Th15
.= Bottom L by A2, LATTICES:20 ; ::_thesis: x "/\" y = Bottom L
hence x "/\" y = Bottom L ; ::_thesis: verum
end;
thus B /\/ FB is B_Lattice by A4; ::_thesis: verum
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
|:f1,f2:| is BinOp of [:D1,D2:]
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 |:f1,f2:| is BinOp of [:D1,D2:] by A3, A4, FUNCT_2:2, XBOOLE_1:1; ::_thesis: verum
end;
end;
theorem Th21: :: FILTER_1:21
for D1, D2 being non empty set
for a1, b1 being Element of D1
for a2, b2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
proof
let D1, D2 be non empty set ; ::_thesis: for a1, b1 being Element of D1
for a2, b2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
let a1, b1 be Element of D1; ::_thesis: for a2, b2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
let a2, b2 be Element of D2; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
let f2 be BinOp of D2; ::_thesis: |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]
A1: dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by FUNCT_2:def_1;
[[a1,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:] ;
hence |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))] by A1, FUNCT_4:55; ::_thesis: verum
end;
scheme :: FILTER_1:sch 4
AuxCart1{ F1() -> non empty set , F2() -> non empty set , P1[ set ] } :
for d being Element of [:F1(),F2():] holds P1[d]
provided
A1: for d1 being Element of F1()
for d2 being Element of F2() holds P1[[d1,d2]]
proof
let d be Element of [:F1(),F2():]; ::_thesis: P1[d]
ex d1 being Element of F1() ex d2 being Element of F2() st d = [d1,d2] by DOMAIN_1:1;
hence P1[d] by A1; ::_thesis: verum
end;
scheme :: FILTER_1:sch 5
AuxCart2{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
for d, d9 being Element of [:F1(),F2():] holds P1[d,d9]
provided
A1: for d1, d19 being Element of F1()
for d2, d29 being Element of F2() holds P1[[d1,d2],[d19,d29]]
proof
let d, d9 be Element of [:F1(),F2():]; ::_thesis: P1[d,d9]
A2: ex d19 being Element of F1() ex d29 being Element of F2() st d9 = [d19,d29] by DOMAIN_1:1;
ex d1 being Element of F1() ex d2 being Element of F2() st d = [d1,d2] by DOMAIN_1:1;
hence P1[d,d9] by A1, A2; ::_thesis: verum
end;
scheme :: FILTER_1:sch 6
AuxCart3{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ] } :
for a, b, c being Element of [:F1(),F2():] holds P1[a,b,c]
provided
A1: for a1, b1, c1 being Element of F1()
for a2, b2, c2 being Element of F2() holds P1[[a1,a2],[b1,b2],[c1,c2]]
proof
let a, b, c be Element of [:F1(),F2():]; ::_thesis: P1[a,b,c]
A2: ex b1 being Element of F1() ex b2 being Element of F2() st b = [b1,b2] by DOMAIN_1:1;
A3: ex c1 being Element of F1() ex c2 being Element of F2() st c = [c1,c2] by DOMAIN_1:1;
ex a1 being Element of F1() ex a2 being Element of F2() st a = [a1,a2] by DOMAIN_1:1;
hence P1[a,b,c] by A1, A2, A3; ::_thesis: verum
end;
theorem Th22: :: FILTER_1:22
for D1, D2 being non empty set
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
proof
let D1, D2 be non empty set ; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f2 be BinOp of D2; ::_thesis: ( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
defpred S1[ set , set ] means |:f1,f2:| . ($1,$2) = |:f1,f2:| . ($2,$1);
thus ( f1 is commutative & f2 is commutative implies |:f1,f2:| is commutative ) ::_thesis: ( |:f1,f2:| is commutative implies ( f1 is commutative & f2 is commutative ) )
proof
assume A1: for a, b being Element of D1 holds f1 . (a,b) = f1 . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: ( not f2 is commutative or |:f1,f2:| is commutative )
assume A2: for a, b being Element of D2 holds f2 . (a,b) = f2 . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: |:f1,f2:| is commutative
A3: for d1, d19 being Element of D1
for d2, d29 being Element of D2 holds S1[[d1,d2],[d19,d29]]
proof
let a1, b1 be Element of D1; ::_thesis: for d2, d29 being Element of D2 holds S1[[a1,d2],[b1,d29]]
let a2, b2 be Element of D2; ::_thesis: S1[[a1,a2],[b1,b2]]
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 ; ::_thesis: verum
end;
thus for a, b being Element of [:D1,D2:] holds S1[a,b] from FILTER_1:sch_5(A3); :: according to BINOP_1:def_2 ::_thesis: verum
end;
assume A4: for a, b being Element of [:D1,D2:] holds |:f1,f2:| . (a,b) = |:f1,f2:| . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: ( f1 is commutative & f2 is commutative )
thus for a, b being Element of D1 holds f1 . (a,b) = f1 . (b,a) :: according to BINOP_1:def_2 ::_thesis: f2 is commutative
proof
set a2 = the Element of D2;
let a1, b1 be Element of D1; ::_thesis: f1 . (a1,b1) = f1 . (b1,a1)
[(f1 . (a1,b1)),(f2 . ( the Element of D2, the Element of D2))] = |:f1,f2:| . ([a1, the Element of D2],[b1, the Element of D2]) by Th21
.= |:f1,f2:| . ([b1, the Element of D2],[a1, the Element of D2]) by A4
.= [(f1 . (b1,a1)),(f2 . ( the Element of D2, the Element of D2))] by Th21 ;
hence f1 . (a1,b1) = f1 . (b1,a1) by XTUPLE_0:1; ::_thesis: verum
end;
set a1 = the Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def_2 ::_thesis: for b1 being Element of D2 holds f2 . (a2,b1) = f2 . (b1,a2)
let b2 be Element of D2; ::_thesis: f2 . (a2,b2) = f2 . (b2,a2)
[(f1 . ( the Element of D1, the Element of D1)),(f2 . (a2,b2))] = |:f1,f2:| . ([ the Element of D1,a2],[ the Element of D1,b2]) by Th21
.= |:f1,f2:| . ([ the Element of D1,b2],[ the Element of D1,a2]) by A4
.= [(f1 . ( the Element of D1, the Element of D1)),(f2 . (b2,a2))] by Th21 ;
hence f2 . (a2,b2) = f2 . (b2,a2) by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th23: :: FILTER_1:23
for D1, D2 being non empty set
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
proof
let D1, D2 be non empty set ; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
let f2 be BinOp of D2; ::_thesis: ( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
thus ( f1 is associative & f2 is associative implies |:f1,f2:| is associative ) ::_thesis: ( |:f1,f2:| is associative implies ( f1 is associative & f2 is associative ) )
proof
defpred S1[ set , set , set ] means |:f1,f2:| . ($1,(|:f1,f2:| . ($2,$3))) = |:f1,f2:| . ((|:f1,f2:| . ($1,$2)),$3);
assume A1: for a, b, c being Element of D1 holds f1 . (a,(f1 . (b,c))) = f1 . ((f1 . (a,b)),c) ; :: according to BINOP_1:def_3 ::_thesis: ( not f2 is associative or |:f1,f2:| is associative )
assume A2: for a, b, c being Element of D2 holds f2 . (a,(f2 . (b,c))) = f2 . ((f2 . (a,b)),c) ; :: according to BINOP_1:def_3 ::_thesis: |:f1,f2:| is associative
A3: now__::_thesis:_for_a1,_b1,_c1_being_Element_of_D1
for_a2,_b2,_c2_being_Element_of_D2_holds_S1[[a1,a2],[b1,b2],[c1,c2]]
let a1, b1, c1 be Element of D1; ::_thesis: for a2, b2, c2 being Element of D2 holds S1[[a1,a2],[b1,b2],[c1,c2]]
let a2, b2, c2 be Element of D2; ::_thesis: S1[[a1,a2],[b1,b2],[c1,c2]]
|: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 S1[[a1,a2],[b1,b2],[c1,c2]] ; ::_thesis: verum
end;
thus for a, b, c being Element of [:D1,D2:] holds S1[a,b,c] from FILTER_1:sch_6(A3); :: according to BINOP_1:def_3 ::_thesis: verum
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) ; :: according to BINOP_1:def_3 ::_thesis: ( f1 is associative & f2 is associative )
thus for a, b, c being Element of D1 holds f1 . (a,(f1 . (b,c))) = f1 . ((f1 . (a,b)),c) :: according to BINOP_1:def_3 ::_thesis: f2 is associative
proof
set a2 = the Element of D2;
let a1, b1, c1 be Element of D1; ::_thesis: f1 . (a1,(f1 . (b1,c1))) = f1 . ((f1 . (a1,b1)),c1)
[(f1 . (a1,(f1 . (b1,c1)))),(f2 . ( the Element of D2,(f2 . ( the Element of D2, the Element of D2))))] = |:f1,f2:| . ([a1, the Element of D2],[(f1 . (b1,c1)),(f2 . ( the Element of D2, the Element of D2))]) by Th21
.= |:f1,f2:| . ([a1, the Element of D2],(|:f1,f2:| . ([b1, the Element of D2],[c1, the Element of D2]))) by Th21
.= |:f1,f2:| . ((|:f1,f2:| . ([a1, the Element of D2],[b1, the Element of D2])),[c1, the Element of D2]) by A4
.= |:f1,f2:| . ([(f1 . (a1,b1)),(f2 . ( the Element of D2, the Element of D2))],[c1, the Element of D2]) by Th21
.= [(f1 . ((f1 . (a1,b1)),c1)),(f2 . ((f2 . ( the Element of D2, the Element of D2)), the Element of D2))] by Th21 ;
hence f1 . (a1,(f1 . (b1,c1))) = f1 . ((f1 . (a1,b1)),c1) by XTUPLE_0:1; ::_thesis: verum
end;
set a1 = the Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def_3 ::_thesis: for b1, b2 being Element of D2 holds f2 . (a2,(f2 . (b1,b2))) = f2 . ((f2 . (a2,b1)),b2)
let b2, c2 be Element of D2; ::_thesis: f2 . (a2,(f2 . (b2,c2))) = f2 . ((f2 . (a2,b2)),c2)
[(f1 . ( the Element of D1,(f1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(f2 . (b2,c2))))] = |:f1,f2:| . ([ the Element of D1,a2],[(f1 . ( the Element of D1, the Element of D1)),(f2 . (b2,c2))]) by Th21
.= |:f1,f2:| . ([ the Element of D1,a2],(|:f1,f2:| . ([ the Element of D1,b2],[ the Element of D1,c2]))) by Th21
.= |:f1,f2:| . ((|:f1,f2:| . ([ the Element of D1,a2],[ the Element of D1,b2])),[ the Element of D1,c2]) by A4
.= |:f1,f2:| . ([(f1 . ( the Element of D1, the Element of D1)),(f2 . (a2,b2))],[ the Element of D1,c2]) by Th21
.= [(f1 . ((f1 . ( the Element of D1, the Element of D1)), the Element of D1)),(f2 . ((f2 . (a2,b2)),c2))] by Th21 ;
hence f2 . (a2,(f2 . (b2,c2))) = f2 . ((f2 . (a2,b2)),c2) by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th24: :: FILTER_1:24
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( 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
let D1, D2 be non empty set ; ::_thesis: for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
let a1 be Element of D1; ::_thesis: for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
let a2 be Element of D2; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
let f2 be BinOp of D2; ::_thesis: ( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
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:| ) ::_thesis: ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| implies ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) )
proof
defpred S1[ set ] means |:f1,f2:| . ([a1,a2],$1) = $1;
assume A1: for b1 being Element of D1 holds f1 . (a1,b1) = b1 ; :: according to BINOP_1:def_16 ::_thesis: ( not a2 is_a_left_unity_wrt f2 or [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
assume A2: for b2 being Element of D2 holds f2 . (a2,b2) = b2 ; :: according to BINOP_1:def_16 ::_thesis: [a1,a2] is_a_left_unity_wrt |:f1,f2:|
A3: now__::_thesis:_for_b1_being_Element_of_D1
for_b2_being_Element_of_D2_holds_S1[[b1,b2]]
let b1 be Element of D1; ::_thesis: for b2 being Element of D2 holds S1[[b1,b2]]
let b2 be Element of D2; ::_thesis: S1[[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 S1[[b1,b2]] ; ::_thesis: verum
end;
thus for a being Element of [:D1,D2:] holds S1[a] from FILTER_1:sch_4(A3); :: according to BINOP_1:def_16 ::_thesis: verum
end;
assume A4: for a being Element of [:D1,D2:] holds |:f1,f2:| . ([a1,a2],a) = a ; :: according to BINOP_1:def_16 ::_thesis: ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 )
thus for b1 being Element of D1 holds f1 . (a1,b1) = b1 :: according to BINOP_1:def_16 ::_thesis: a2 is_a_left_unity_wrt f2
proof
let b1 be Element of D1; ::_thesis: f1 . (a1,b1) = b1
set b2 = the Element of D2;
[(f1 . (a1,b1)),(f2 . (a2, the Element of D2))] = |:f1,f2:| . ([a1,a2],[b1, the Element of D2]) by Th21
.= [b1, the Element of D2] by A4 ;
hence f1 . (a1,b1) = b1 by XTUPLE_0:1; ::_thesis: verum
end;
set b1 = the Element of D1;
let b2 be Element of D2; :: according to BINOP_1:def_16 ::_thesis: f2 . (a2,b2) = b2
[(f1 . (a1, the Element of D1)),(f2 . (a2,b2))] = |:f1,f2:| . ([a1,a2],[ the Element of D1,b2]) by Th21
.= [ the Element of D1,b2] by A4 ;
hence f2 . (a2,b2) = b2 by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th25: :: FILTER_1:25
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( 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
let D1, D2 be non empty set ; ::_thesis: for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
let a1 be Element of D1; ::_thesis: for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
let a2 be Element of D2; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds
( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
let f2 be BinOp of D2; ::_thesis: ( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
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:| ) ::_thesis: ( [a1,a2] is_a_right_unity_wrt |:f1,f2:| implies ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) )
proof
defpred S1[ set ] means |:f1,f2:| . ($1,[a1,a2]) = $1;
assume A1: for b1 being Element of D1 holds f1 . (b1,a1) = b1 ; :: according to BINOP_1:def_17 ::_thesis: ( not a2 is_a_right_unity_wrt f2 or [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
assume A2: for b2 being Element of D2 holds f2 . (b2,a2) = b2 ; :: according to BINOP_1:def_17 ::_thesis: [a1,a2] is_a_right_unity_wrt |:f1,f2:|
A3: now__::_thesis:_for_b1_being_Element_of_D1
for_b2_being_Element_of_D2_holds_S1[[b1,b2]]
let b1 be Element of D1; ::_thesis: for b2 being Element of D2 holds S1[[b1,b2]]
let b2 be Element of D2; ::_thesis: S1[[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 S1[[b1,b2]] ; ::_thesis: verum
end;
thus for a being Element of [:D1,D2:] holds S1[a] from FILTER_1:sch_4(A3); :: according to BINOP_1:def_17 ::_thesis: verum
end;
assume A4: for a being Element of [:D1,D2:] holds |:f1,f2:| . (a,[a1,a2]) = a ; :: according to BINOP_1:def_17 ::_thesis: ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 )
thus for b1 being Element of D1 holds f1 . (b1,a1) = b1 :: according to BINOP_1:def_17 ::_thesis: a2 is_a_right_unity_wrt f2
proof
let b1 be Element of D1; ::_thesis: f1 . (b1,a1) = b1
set b2 = the Element of D2;
[(f1 . (b1,a1)),(f2 . ( the Element of D2,a2))] = |:f1,f2:| . ([b1, the Element of D2],[a1,a2]) by Th21
.= [b1, the Element of D2] by A4 ;
hence f1 . (b1,a1) = b1 by XTUPLE_0:1; ::_thesis: verum
end;
set b1 = the Element of D1;
let b2 be Element of D2; :: according to BINOP_1:def_17 ::_thesis: f2 . (b2,a2) = b2
[(f1 . ( the Element of D1,a1)),(f2 . (b2,a2))] = |:f1,f2:| . ([ the Element of D1,b2],[a1,a2]) by Th21
.= [ the Element of D1,b2] by A4 ;
hence f2 . (b2,a2) = b2 by XTUPLE_0:1; ::_thesis: verum
end;
theorem :: FILTER_1:26
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
proof
let D1, D2 be non empty set ; ::_thesis: for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let a1 be Element of D1; ::_thesis: for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let a2 be Element of D2; ::_thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let f1 be BinOp of D1; ::_thesis: for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let f2 be BinOp of D2; ::_thesis: ( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
thus ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 implies [a1,a2] is_a_unity_wrt |:f1,f2:| ) ::_thesis: ( [a1,a2] is_a_unity_wrt |:f1,f2:| implies ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) )
proof
assume that
A1: a1 is_a_left_unity_wrt f1 and
A2: a1 is_a_right_unity_wrt f1 and
A3: a2 is_a_left_unity_wrt f2 and
A4: a2 is_a_right_unity_wrt f2 ; :: according to BINOP_1:def_7 ::_thesis: [a1,a2] is_a_unity_wrt |:f1,f2:|
thus ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| & [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) by A1, A2, A3, A4, Th24, Th25; :: according to BINOP_1:def_7 ::_thesis: verum
end;
assume that
A5: [a1,a2] is_a_left_unity_wrt |:f1,f2:| and
A6: [a1,a2] is_a_right_unity_wrt |:f1,f2:| ; :: according to BINOP_1:def_7 ::_thesis: ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 )
thus ( 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 A5, A6, Th24, Th25; :: according to BINOP_1:def_7 ::_thesis: verum
end;
theorem Th27: :: FILTER_1:27
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
proof
let D1, D2 be non empty set ; ::_thesis: for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
let f1, g1 be BinOp of D1; ::_thesis: for f2, g2 being BinOp of D2 holds
( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
let f2, g2 be BinOp of D2; ::_thesis: ( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
thus ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 implies |:f1,f2:| is_left_distributive_wrt |:g1,g2:| ) ::_thesis: ( |:f1,f2:| is_left_distributive_wrt |:g1,g2:| implies ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) )
proof
defpred S1[ 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 being Element of D1 holds f1 . (a1,(g1 . (b1,c1))) = g1 . ((f1 . (a1,b1)),(f1 . (a1,c1))) ; :: according to BINOP_1:def_18 ::_thesis: ( not f2 is_left_distributive_wrt g2 or |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
assume A2: for a2, b2, c2 being Element of D2 holds f2 . (a2,(g2 . (b2,c2))) = g2 . ((f2 . (a2,b2)),(f2 . (a2,c2))) ; :: according to BINOP_1:def_18 ::_thesis: |:f1,f2:| is_left_distributive_wrt |:g1,g2:|
A3: now__::_thesis:_for_a1,_b1,_c1_being_Element_of_D1
for_a2,_b2,_c2_being_Element_of_D2_holds_S1[[a1,a2],[b1,b2],[c1,c2]]
let a1, b1, c1 be Element of D1; ::_thesis: for a2, b2, c2 being Element of D2 holds S1[[a1,a2],[b1,b2],[c1,c2]]
let a2, b2, c2 be Element of D2; ::_thesis: S1[[a1,a2],[b1,b2],[c1,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 S1[[a1,a2],[b1,b2],[c1,c2]] ; ::_thesis: verum
end;
thus for a, b, c being Element of [:D1,D2:] holds S1[a,b,c] from FILTER_1:sch_6(A3); :: according to BINOP_1:def_18 ::_thesis: verum
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))) ; :: according to BINOP_1:def_18 ::_thesis: ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 )
A5: now__::_thesis:_for_a1,_b1,_c1_being_Element_of_D1
for_a2,_b2,_c2_being_Element_of_D2_holds_[(f1_._(a1,(g1_._(b1,c1)))),(f2_._(a2,(g2_._(b2,c2))))]_=_[(g1_._((f1_._(a1,b1)),(f1_._(a1,c1)))),(g2_._((f2_._(a2,b2)),(f2_._(a2,c2))))]
let a1, b1, c1 be Element of D1; ::_thesis: for a2, b2, c2 being Element of D2 holds [(f1 . (a1,(g1 . (b1,c1)))),(f2 . (a2,(g2 . (b2,c2))))] = [(g1 . ((f1 . (a1,b1)),(f1 . (a1,c1)))),(g2 . ((f2 . (a2,b2)),(f2 . (a2,c2))))]
let a2, b2, c2 be Element of D2; ::_thesis: [(f1 . (a1,(g1 . (b1,c1)))),(f2 . (a2,(g2 . (b2,c2))))] = [(g1 . ((f1 . (a1,b1)),(f1 . (a1,c1)))),(g2 . ((f2 . (a2,b2)),(f2 . (a2,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 ; ::_thesis: verum
end;
thus for a1, b1, c1 being Element of D1 holds f1 . (a1,(g1 . (b1,c1))) = g1 . ((f1 . (a1,b1)),(f1 . (a1,c1))) :: according to BINOP_1:def_18 ::_thesis: f2 is_left_distributive_wrt g2
proof
set a2 = the Element of D2;
let a1, b1, c1 be Element of D1; ::_thesis: f1 . (a1,(g1 . (b1,c1))) = g1 . ((f1 . (a1,b1)),(f1 . (a1,c1)))
[(f1 . (a1,(g1 . (b1,c1)))),(f2 . ( the Element of D2,(g2 . ( the Element of D2, the Element of D2))))] = [(g1 . ((f1 . (a1,b1)),(f1 . (a1,c1)))),(g2 . ((f2 . ( the Element of D2, the Element of D2)),(f2 . ( the Element of D2, the Element of D2))))] by A5;
hence f1 . (a1,(g1 . (b1,c1))) = g1 . ((f1 . (a1,b1)),(f1 . (a1,c1))) by XTUPLE_0:1; ::_thesis: verum
end;
set a1 = the Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def_18 ::_thesis: for b1, b2 being Element of D2 holds f2 . (a2,(g2 . (b1,b2))) = g2 . ((f2 . (a2,b1)),(f2 . (a2,b2)))
let b2, c2 be Element of D2; ::_thesis: f2 . (a2,(g2 . (b2,c2))) = g2 . ((f2 . (a2,b2)),(f2 . (a2,c2)))
[(f1 . ( the Element of D1,(g1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(g2 . (b2,c2))))] = [(g1 . ((f1 . ( the Element of D1, the Element of D1)),(f1 . ( the Element of D1, the Element of D1)))),(g2 . ((f2 . (a2,b2)),(f2 . (a2,c2))))] by A5;
hence f2 . (a2,(g2 . (b2,c2))) = g2 . ((f2 . (a2,b2)),(f2 . (a2,c2))) by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th28: :: FILTER_1:28
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
proof
let D1, D2 be non empty set ; ::_thesis: for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
let f1, g1 be BinOp of D1; ::_thesis: for f2, g2 being BinOp of D2 holds
( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
let f2, g2 be BinOp of D2; ::_thesis: ( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
thus ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 implies |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ) ::_thesis: ( |:f1,f2:| is_right_distributive_wrt |:g1,g2:| implies ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) )
proof
defpred S1[ 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 being Element of D1 holds f1 . ((g1 . (b1,c1)),a1) = g1 . ((f1 . (b1,a1)),(f1 . (c1,a1))) ; :: according to BINOP_1:def_19 ::_thesis: ( not f2 is_right_distributive_wrt g2 or |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
assume A2: for b2, c2, a2 being Element of D2 holds f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))) ; :: according to BINOP_1:def_19 ::_thesis: |:f1,f2:| is_right_distributive_wrt |:g1,g2:|
A3: now__::_thesis:_for_a1,_b1,_c1_being_Element_of_D1
for_a2,_b2,_c2_being_Element_of_D2_holds_S1[[a1,a2],[b1,b2],[c1,c2]]
let a1, b1, c1 be Element of D1; ::_thesis: for a2, b2, c2 being Element of D2 holds S1[[a1,a2],[b1,b2],[c1,c2]]
let a2, b2, c2 be Element of D2; ::_thesis: S1[[a1,a2],[b1,b2],[c1,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 S1[[a1,a2],[b1,b2],[c1,c2]] ; ::_thesis: verum
end;
for a, b, c being Element of [:D1,D2:] holds S1[a,b,c] from FILTER_1:sch_6(A3);
then for b, c, a being Element of [:D1,D2:] holds S1[a,b,c] ;
hence |:f1,f2:| is_right_distributive_wrt |:g1,g2:| by BINOP_1:def_19; ::_thesis: verum
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))) ; :: according to BINOP_1:def_19 ::_thesis: ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 )
A5: now__::_thesis:_for_a1,_b1,_c1_being_Element_of_D1
for_a2,_b2,_c2_being_Element_of_D2_holds_[(f1_._((g1_._(b1,c1)),a1)),(f2_._((g2_._(b2,c2)),a2))]_=_[(g1_._((f1_._(b1,a1)),(f1_._(c1,a1)))),(g2_._((f2_._(b2,a2)),(f2_._(c2,a2))))]
let a1, b1, c1 be Element of D1; ::_thesis: for a2, b2, c2 being Element of D2 holds [(f1 . ((g1 . (b1,c1)),a1)),(f2 . ((g2 . (b2,c2)),a2))] = [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))]
let a2, b2, c2 be Element of D2; ::_thesis: [(f1 . ((g1 . (b1,c1)),a1)),(f2 . ((g2 . (b2,c2)),a2))] = [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))]
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 ; ::_thesis: verum
end;
thus for b1, c1, a1 being Element of D1 holds f1 . ((g1 . (b1,c1)),a1) = g1 . ((f1 . (b1,a1)),(f1 . (c1,a1))) :: according to BINOP_1:def_19 ::_thesis: f2 is_right_distributive_wrt g2
proof
set a2 = the Element of D2;
let b1, c1, a1 be Element of D1; ::_thesis: f1 . ((g1 . (b1,c1)),a1) = g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))
[(f1 . ((g1 . (b1,c1)),a1)),(f2 . ((g2 . ( the Element of D2, the Element of D2)), the Element of D2))] = [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(g2 . ((f2 . ( the Element of D2, the Element of D2)),(f2 . ( the Element of D2, the Element of D2))))] by A5;
hence f1 . ((g1 . (b1,c1)),a1) = g1 . ((f1 . (b1,a1)),(f1 . (c1,a1))) by XTUPLE_0:1; ::_thesis: verum
end;
set a1 = the Element of D1;
let b2 be Element of D2; :: according to BINOP_1:def_19 ::_thesis: for b1, b2 being Element of D2 holds f2 . ((g2 . (b2,b1)),b2) = g2 . ((f2 . (b2,b2)),(f2 . (b1,b2)))
let c2, a2 be Element of D2; ::_thesis: f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2)))
[(f1 . ((g1 . ( the Element of D1, the Element of D1)), the Element of D1)),(f2 . ((g2 . (b2,c2)),a2))] = [(g1 . ((f1 . ( the Element of D1, the Element of D1)),(f1 . ( the Element of D1, the Element of D1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))] by A5;
hence f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))) by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th29: :: FILTER_1:29
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| )
proof
let D1, D2 be non empty set ; ::_thesis: for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| )
let f1, g1 be BinOp of D1; ::_thesis: for f2, g2 being BinOp of D2 holds
( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| )
let f2, g2 be BinOp of D2; ::_thesis: ( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| )
thus ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 implies |:f1,f2:| is_distributive_wrt |:g1,g2:| ) ::_thesis: ( |:f1,f2:| is_distributive_wrt |:g1,g2:| implies ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) )
proof
assume that
A1: f1 is_left_distributive_wrt g1 and
A2: f1 is_right_distributive_wrt g1 and
A3: f2 is_left_distributive_wrt g2 and
A4: f2 is_right_distributive_wrt g2 ; :: according to BINOP_1:def_11 ::_thesis: |:f1,f2:| is_distributive_wrt |:g1,g2:|
thus ( |:f1,f2:| is_left_distributive_wrt |:g1,g2:| & |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ) by A1, A2, A3, A4, Th27, Th28; :: according to BINOP_1:def_11 ::_thesis: verum
end;
assume that
A5: |:f1,f2:| is_left_distributive_wrt |:g1,g2:| and
A6: |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ; :: according to BINOP_1:def_11 ::_thesis: ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 )
thus ( 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 A5, A6, Th27, Th28; :: according to BINOP_1:def_11 ::_thesis: verum
end;
theorem Th30: :: FILTER_1:30
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
proof
let D1, D2 be non empty set ; ::_thesis: for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
let f1, g1 be BinOp of D1; ::_thesis: for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
let f2, g2 be BinOp of D2; ::_thesis: ( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
defpred S1[ set , set ] means |:f1,f2:| . ($1,(|:g1,g2:| . ($1,$2))) = $1;
thus ( f1 absorbs g1 & f2 absorbs g2 implies |:f1,f2:| absorbs |:g1,g2:| ) ::_thesis: ( |:f1,f2:| absorbs |:g1,g2:| implies ( f1 absorbs g1 & f2 absorbs g2 ) )
proof
assume A1: for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1 ; :: according to LATTICE2:def_1 ::_thesis: ( not f2 absorbs g2 or |:f1,f2:| absorbs |:g1,g2:| )
assume A2: for a2, b2 being Element of D2 holds f2 . (a2,(g2 . (a2,b2))) = a2 ; :: according to LATTICE2:def_1 ::_thesis: |:f1,f2:| absorbs |:g1,g2:|
A3: for d1, d19 being Element of D1
for d2, d29 being Element of D2 holds S1[[d1,d2],[d19,d29]]
proof
let a1, b1 be Element of D1; ::_thesis: for d2, d29 being Element of D2 holds S1[[a1,d2],[b1,d29]]
let a2, b2 be Element of D2; ::_thesis: S1[[a1,a2],[b1,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 ; ::_thesis: verum
end;
thus for a, b being Element of [:D1,D2:] holds S1[a,b] from FILTER_1:sch_5(A3); :: according to LATTICE2:def_1 ::_thesis: verum
end;
assume A4: for a, b being Element of [:D1,D2:] holds |:f1,f2:| . (a,(|:g1,g2:| . (a,b))) = a ; :: according to LATTICE2:def_1 ::_thesis: ( f1 absorbs g1 & f2 absorbs g2 )
thus for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1 :: according to LATTICE2:def_1 ::_thesis: f2 absorbs g2
proof
set a2 = the Element of D2;
let a1, b1 be Element of D1; ::_thesis: f1 . (a1,(g1 . (a1,b1))) = a1
[a1, the Element of D2] = |:f1,f2:| . ([a1, the Element of D2],(|:g1,g2:| . ([a1, the Element of D2],[b1, the Element of D2]))) by A4
.= |:f1,f2:| . ([a1, the Element of D2],[(g1 . (a1,b1)),(g2 . ( the Element of D2, the Element of D2))]) by Th21
.= [(f1 . (a1,(g1 . (a1,b1)))),(f2 . ( the Element of D2,(g2 . ( the Element of D2, the Element of D2))))] by Th21 ;
hence f1 . (a1,(g1 . (a1,b1))) = a1 by XTUPLE_0:1; ::_thesis: verum
end;
set a1 = the Element of D1;
let a2 be Element of D2; :: according to LATTICE2:def_1 ::_thesis: for b1 being Element of D2 holds f2 . (a2,(g2 . (a2,b1))) = a2
let b2 be Element of D2; ::_thesis: f2 . (a2,(g2 . (a2,b2))) = a2
[ the Element of D1,a2] = |:f1,f2:| . ([ the Element of D1,a2],(|:g1,g2:| . ([ the Element of D1,a2],[ the Element of D1,b2]))) by A4
.= |:f1,f2:| . ([ the Element of D1,a2],[(g1 . ( the Element of D1, the Element of D1)),(g2 . (a2,b2))]) by Th21
.= [(f1 . ( the Element of D1,(g1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(g2 . (a2,b2))))] by Th21 ;
hence f2 . (a2,(g2 . (a2,b2))) = a2 by XTUPLE_0:1; ::_thesis: verum
end;
definition
let L1, L2 be non empty LattStr ;
func[:L1,L2:] -> strict LattStr equals :: FILTER_1:def 7
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
coherence
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:| #) is strict LattStr ;
;
end;
:: deftheorem defines [: FILTER_1:def_7_:_
for L1, L2 being non empty LattStr holds [: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:| #);
registration
let L1, L2 be non empty LattStr ;
cluster[:L1,L2:] -> non empty strict ;
coherence
not [:L1,L2:] is empty ;
end;
definition
let L be Lattice;
func LattRel L -> Relation equals :: FILTER_1:def 8
{ [p,q] where p, q is Element of L : p [= q } ;
coherence
{ [p,q] where p, q is Element of L : p [= q } is Relation
proof
now__::_thesis:_for_x_being_set_st_x_in__{__[p,q]_where_p,_q_is_Element_of_L_:_p_[=_q__}__holds_
ex_x1,_x2_being_set_st_x_=_[x1,x2]
let x be set ; ::_thesis: ( x in { [p,q] where p, q is Element of L : p [= q } implies ex x1, x2 being set st x = [x1,x2] )
assume x in { [p,q] where p, q is Element of L : p [= q } ; ::_thesis: ex x1, x2 being set st x = [x1,x2]
then ex p, q being Element of L st
( x = [p,q] & p [= q ) ;
hence ex x1, x2 being set st x = [x1,x2] ; ::_thesis: verum
end;
hence { [p,q] where p, q is Element of L : p [= q } is Relation by RELAT_1:def_1; ::_thesis: verum
end;
end;
:: deftheorem defines LattRel FILTER_1:def_8_:_
for L being Lattice holds LattRel L = { [p,q] where p, q is Element of L : p [= q } ;
theorem Th31: :: FILTER_1:31
for L being Lattice
for p, q being Element of L holds
( [p,q] in LattRel L iff p [= q )
proof
let L be Lattice; ::_thesis: for p, q being Element of L holds
( [p,q] in LattRel L iff p [= q )
let p, q be Element of L; ::_thesis: ( [p,q] in LattRel L iff p [= q )
thus ( [p,q] in LattRel L implies p [= q ) ::_thesis: ( p [= q implies [p,q] in LattRel L )
proof
assume [p,q] in LattRel L ; ::_thesis: p [= q
then consider r, s being Element of L such that
A1: [p,q] = [r,s] and
A2: r [= s ;
p = r by A1, XTUPLE_0:1;
hence p [= q by A1, A2, XTUPLE_0:1; ::_thesis: verum
end;
thus ( p [= q implies [p,q] in LattRel L ) ; ::_thesis: verum
end;
theorem Th32: :: FILTER_1:32
for L being Lattice holds
( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )
proof
let L be Lattice; ::_thesis: ( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_L_implies_ex_y_being_set_st_[x,y]_in_LattRel_L_)_&_(_ex_y_being_set_st_[x,y]_in_LattRel_L_implies_x_in_the_carrier_of_L_)_)
let x be set ; ::_thesis: ( ( x in the carrier of L implies ex y being set st [x,y] in LattRel L ) & ( ex y being set st [x,y] in LattRel L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being set st [x,y] in LattRel L ) ::_thesis: ( ex y being set st [x,y] in LattRel L implies x in the carrier of L )
proof
assume x in the carrier of L ; ::_thesis: ex y being set st [x,y] in LattRel L
then reconsider p = x as Element of L ;
[p,p] in LattRel L ;
hence ex y being set st [x,y] in LattRel L ; ::_thesis: verum
end;
given y being set such that A1: [x,y] in LattRel L ; ::_thesis: x in the carrier of L
consider p, q being Element of L 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 ; ::_thesis: verum
end;
hence A3: dom (LattRel L) = the carrier of L by XTUPLE_0:def_12; ::_thesis: ( rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_L_implies_ex_y_being_set_st_[y,x]_in_LattRel_L_)_&_(_ex_y_being_set_st_[y,x]_in_LattRel_L_implies_x_in_the_carrier_of_L_)_)
let x be set ; ::_thesis: ( ( x in the carrier of L implies ex y being set st [y,x] in LattRel L ) & ( ex y being set st [y,x] in LattRel L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being set st [y,x] in LattRel L ) ::_thesis: ( ex y being set st [y,x] in LattRel L implies x in the carrier of L )
proof
assume x in the carrier of L ; ::_thesis: ex y being set st [y,x] in LattRel L
then reconsider p = x as Element of L ;
[p,p] in LattRel L ;
hence ex y being set st [y,x] in LattRel L ; ::_thesis: verum
end;
given y being set such that A4: [y,x] in LattRel L ; ::_thesis: x in the carrier of L
consider p, q being Element of L 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 ; ::_thesis: verum
end;
hence rng (LattRel L) = the carrier of L by XTUPLE_0:def_13; ::_thesis: field (LattRel L) = the carrier of L
hence field (LattRel L) = the carrier of L \/ the carrier of L by A3, RELAT_1:def_6
.= the carrier of L ;
::_thesis: verum
end;
definition
let L1, L2 be Lattice;
predL1,L2 are_isomorphic means :: FILTER_1:def 9
LattRel L1, LattRel L2 are_isomorphic ;
reflexivity
for L1 being Lattice holds LattRel L1, LattRel L1 are_isomorphic by WELLORD1:38;
symmetry
for L1, L2 being Lattice st LattRel L1, LattRel L2 are_isomorphic holds
LattRel L2, LattRel L1 are_isomorphic by WELLORD1:40;
end;
:: deftheorem defines are_isomorphic FILTER_1:def_9_:_
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff LattRel L1, LattRel L2 are_isomorphic );
registration
let L1, L2 be Lattice;
cluster[:L1,L2:] -> strict Lattice-like ;
coherence
[:L1,L2:] is Lattice-like
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: H1(L2) absorbs H2(L2) by LATTICE2:26;
H1(L1) absorbs H2(L1) by LATTICE2:26;
then A2: H1(LL) absorbs H2(LL) by A1, Th30;
A3: H1(LL) is associative by Th23;
A4: H2(L2) absorbs H1(L2) by LATTICE2:27;
H2(L1) absorbs H1(L1) by LATTICE2:27;
then A5: H2(LL) absorbs H1(LL) by A4, Th30;
A6: H2(LL) is commutative by Th22;
A7: H2(LL) is associative by Th23;
H1(LL) is commutative by Th22;
hence [:L1,L2:] is Lattice-like by A3, A6, A7, A2, A5, LATTICE2:11; ::_thesis: verum
end;
end;
theorem :: FILTER_1:33
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; ::_thesis: ( L1,L2 are_isomorphic & L2,L3 are_isomorphic implies L1,L3 are_isomorphic )
assume that
A1: LattRel L1, LattRel L2 are_isomorphic and
A2: LattRel L2, LattRel L3 are_isomorphic ; :: according to FILTER_1:def_9 ::_thesis: L1,L3 are_isomorphic
thus LattRel L1, LattRel L3 are_isomorphic by A1, A2, WELLORD1:42; :: according to FILTER_1:def_9 ::_thesis: verum
end;
theorem :: FILTER_1:34
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 ; ::_thesis: ( [:L1,L2:] is Lattice implies ( L1 is Lattice & L2 is Lattice ) )
assume A1: [:L1,L2:] is Lattice ; ::_thesis: ( L1 is Lattice & L2 is Lattice )
A2: H1(L1) is associative by A1, Th23;
A3: H2(L2) is associative by A1, Th23;
A4: H2(L2) is commutative by A1, Th22;
reconsider LL = LattStr(# [: the carrier of L1, the carrier of L2:],|:H1(L1),H1(L2):|,|:H2(L1),H2(L2):| #) as non empty LattStr ;
A5: H1(LL) absorbs H2(LL) by A1, LATTICE2:26;
then A6: H1(L1) absorbs H2(L1) by Th30;
A7: H1(L2) is associative by A1, Th23;
A8: H1(L2) is commutative by A1, Th22;
A9: H2(L1) is associative by A1, Th23;
A10: H2(L1) is commutative by A1, Th22;
A11: H2(LL) absorbs H1(LL) by A1, LATTICE2:27;
then A12: H2(L1) absorbs H1(L1) by Th30;
A13: H2(L2) absorbs H1(L2) by A11, Th30;
A14: H1(L2) absorbs H2(L2) by A5, Th30;
H1(L1) is commutative by A1, Th22;
hence ( L1 is Lattice & L2 is Lattice ) by A2, A10, A9, A6, A12, A8, A7, A4, A3, A14, A13, LATTICE2:11; ::_thesis: verum
end;
definition
let L1, L2 be Lattice;
let a be Element of L1;
let b be Element of L2;
:: original: [
redefine func[a,b] -> Element of [:L1,L2:];
coherence
[a,b] is Element of [:L1,L2:]
proof
[a,b] is Element of [: the carrier of L1, the carrier of L2:] ;
hence [a,b] is Element of [:L1,L2:] ; ::_thesis: verum
end;
end;
theorem :: FILTER_1:35
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] "\/" [q1,q2] = [(p1 "\/" q1),(p2 "\/" q2)] & [p1,p2] "/\" [q1,q2] = [(p1 "/\" q1),(p2 "/\" q2)] ) by Th21;
theorem Th36: :: FILTER_1:36
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
proof
let L1, L2 be Lattice; ::_thesis: for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
let p1, q1 be Element of L1; ::_thesis: for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
let p2, q2 be Element of L2; ::_thesis: ( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
thus ( [p1,p2] [= [q1,q2] implies ( p1 [= q1 & p2 [= q2 ) ) ::_thesis: ( p1 [= q1 & p2 [= q2 implies [p1,p2] [= [q1,q2] )
proof
assume [p1,p2] "\/" [q1,q2] = [q1,q2] ; :: according to LATTICES:def_3 ::_thesis: ( p1 [= q1 & p2 [= q2 )
then [(p1 "\/" q1),(p2 "\/" q2)] = [q1,q2] by Th21;
hence ( p1 "\/" q1 = q1 & p2 "\/" q2 = q2 ) by XTUPLE_0:1; :: according to LATTICES:def_3 ::_thesis: verum
end;
assume that
A1: p1 "\/" q1 = q1 and
A2: p2 "\/" q2 = q2 ; :: according to LATTICES:def_3 ::_thesis: [p1,p2] [= [q1,q2]
thus [p1,p2] "\/" [q1,q2] = [q1,q2] by A1, A2, Th21; :: according to LATTICES:def_3 ::_thesis: verum
end;
theorem :: FILTER_1:37
for L1, L2 being Lattice holds
( ( L1 is modular & L2 is modular ) iff [:L1,L2:] is modular )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is modular & L2 is modular ) iff [:L1,L2:] is modular )
thus ( L1 is modular & L2 is modular implies [:L1,L2:] is modular ) ::_thesis: ( [:L1,L2:] is modular implies ( L1 is modular & L2 is modular ) )
proof
assume A1: for p1, q1, r1 being Element of L1 st p1 [= r1 holds
p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1 ; :: according to LATTICES:def_12 ::_thesis: ( not L2 is modular or [:L1,L2:] is modular )
assume A2: for p2, q2, r2 being Element of L2 st p2 [= r2 holds
p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2 ; :: according to LATTICES:def_12 ::_thesis: [:L1,L2:] is modular
let a, b, c be Element of [:L1,L2:]; :: according to LATTICES:def_12 ::_thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A3: a [= c ; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
consider q1 being Element of L1, q2 being Element of L2 such that
A4: b = [q1,q2] by DOMAIN_1:1;
consider p1 being Element of L1, p2 being Element of L2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
consider r1 being Element of L1, r2 being Element of L2 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 ; ::_thesis: verum
end;
assume A9: for a, b, c being Element of [:L1,L2:] st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def_12 ::_thesis: ( L1 is modular & L2 is modular )
thus L1 is modular ::_thesis: L2 is modular
proof
set p2 = the Element of L2;
let p1 be Element of L1; :: according to LATTICES:def_12 ::_thesis: for b1, b2 being Element of the carrier of L1 holds
( not p1 [= b2 or p1 "\/" (b1 "/\" b2) = (p1 "\/" b1) "/\" b2 )
let q1, r1 be Element of L1; ::_thesis: ( not p1 [= r1 or p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1 )
assume p1 [= r1 ; ::_thesis: p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1
then [p1, the Element of L2] [= [r1, the Element of L2] by Th36;
then A10: [p1, the Element of L2] "\/" ([q1, the Element of L2] "/\" [r1, the Element of L2]) = ([p1, the Element of L2] "\/" [q1, the Element of L2]) "/\" [r1, the Element of L2] by A9;
A11: [p1, the Element of L2] "\/" [q1, the Element of L2] = [(p1 "\/" q1),( the Element of L2 "\/" the Element of L2)] by Th21;
A12: [(p1 "\/" q1),( the Element of L2 "\/" the Element of L2)] "/\" [r1, the Element of L2] = [((p1 "\/" q1) "/\" r1),(( the Element of L2 "\/" the Element of L2) "/\" the Element of L2)] by Th21;
A13: [p1, the Element of L2] "\/" [(q1 "/\" r1),( the Element of L2 "/\" the Element of L2)] = [(p1 "\/" (q1 "/\" r1)),( the Element of L2 "\/" ( the Element of L2 "/\" the Element of L2))] by Th21;
[q1, the Element of L2] "/\" [r1, the Element of L2] = [(q1 "/\" r1),( the Element of L2 "/\" the Element of L2)] by Th21;
hence p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1 by A10, A11, A13, A12, XTUPLE_0:1; ::_thesis: verum
end;
set p1 = the Element of L1;
let p2 be Element of L2; :: according to LATTICES:def_12 ::_thesis: for b1, b2 being Element of the carrier of L2 holds
( not p2 [= b2 or p2 "\/" (b1 "/\" b2) = (p2 "\/" b1) "/\" b2 )
let q2, r2 be Element of L2; ::_thesis: ( not p2 [= r2 or p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2 )
assume p2 [= r2 ; ::_thesis: p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2
then [ the Element of L1,p2] [= [ the Element of L1,r2] by Th36;
then A14: [ the Element of L1,p2] "\/" ([ the Element of L1,q2] "/\" [ the Element of L1,r2]) = ([ the Element of L1,p2] "\/" [ the Element of L1,q2]) "/\" [ the Element of L1,r2] by A9;
A15: [ the Element of L1,p2] "\/" [ the Element of L1,q2] = [( the Element of L1 "\/" the Element of L1),(p2 "\/" q2)] by Th21;
A16: [( the Element of L1 "\/" the Element of L1),(p2 "\/" q2)] "/\" [ the Element of L1,r2] = [(( the Element of L1 "\/" the Element of L1) "/\" the Element of L1),((p2 "\/" q2) "/\" r2)] by Th21;
A17: [ the Element of L1,p2] "\/" [( the Element of L1 "/\" the Element of L1),(q2 "/\" r2)] = [( the Element of L1 "\/" ( the Element of L1 "/\" the Element of L1)),(p2 "\/" (q2 "/\" r2))] by Th21;
[ the Element of L1,q2] "/\" [ the Element of L1,r2] = [( the Element of L1 "/\" the Element of L1),(q2 "/\" r2)] by Th21;
hence p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2 by A14, A15, A17, A16, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th38: :: FILTER_1:38
for L1, L2 being Lattice holds
( ( L1 is D_Lattice & L2 is D_Lattice ) iff [:L1,L2:] is D_Lattice )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is D_Lattice & L2 is D_Lattice ) iff [:L1,L2:] is D_Lattice )
thus ( L1 is D_Lattice & L2 is D_Lattice implies [:L1,L2:] is D_Lattice ) ::_thesis: ( [:L1,L2:] is D_Lattice implies ( L1 is D_Lattice & L2 is D_Lattice ) )
proof
assume that
A1: L1 is D_Lattice and
A2: L2 is D_Lattice ; ::_thesis: [:L1,L2:] is D_Lattice
A3: H1(L2) is_distributive_wrt H2(L2) by A2, LATTICE2:21;
H1(L1) is_distributive_wrt H2(L1) by A1, LATTICE2:21;
then |:H1(L1),H1(L2):| is_distributive_wrt |:H2(L1),H2(L2):| by A3, Th29;
hence [:L1,L2:] is D_Lattice by LATTICE2:22; ::_thesis: verum
end;
assume [:L1,L2:] is D_Lattice ; ::_thesis: ( L1 is D_Lattice & L2 is D_Lattice )
then A4: H1([:L1,L2:]) is_distributive_wrt H2([:L1,L2:]) by LATTICE2:21;
then A5: H1(L2) is_distributive_wrt H2(L2) by Th29;
H1(L1) is_distributive_wrt H2(L1) by A4, Th29;
hence ( L1 is D_Lattice & L2 is D_Lattice ) by A5, LATTICE2:22; ::_thesis: verum
end;
theorem Th39: :: FILTER_1:39
for L1, L2 being Lattice holds
( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )
thus ( L1 is lower-bounded & L2 is lower-bounded implies [:L1,L2:] is lower-bounded ) ::_thesis: ( [:L1,L2:] is lower-bounded implies ( L1 is lower-bounded & L2 is lower-bounded ) )
proof
given p1 being Element of L1 such that A1: for q1 being Element of L1 holds
( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 ) ; :: according to LATTICES:def_13 ::_thesis: ( not L2 is lower-bounded or [:L1,L2:] is lower-bounded )
given p2 being Element of L2 such that A2: for q2 being Element of L2 holds
( p2 "/\" q2 = p2 & q2 "/\" p2 = p2 ) ; :: according to LATTICES:def_13 ::_thesis: [:L1,L2:] is lower-bounded
take a = [p1,p2]; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of [:L1,L2:] holds
( a "/\" b1 = a & b1 "/\" a = a )
let b be Element of [:L1,L2:]; ::_thesis: ( a "/\" b = a & b "/\" a = a )
consider q1 being Element of L1, q2 being Element of L2 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 ; ::_thesis: b "/\" a = a
hence b "/\" a = a ; ::_thesis: verum
end;
given a being Element of [:L1,L2:] such that A4: for b being Element of [:L1,L2:] holds
( a "/\" b = a & b "/\" a = a ) ; :: according to LATTICES:def_13 ::_thesis: ( L1 is lower-bounded & L2 is lower-bounded )
consider p1 being Element of L1, p2 being Element of L2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
thus L1 is lower-bounded ::_thesis: L2 is lower-bounded
proof
set q2 = the Element of L2;
take p1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L1 holds
( p1 "/\" b1 = p1 & b1 "/\" p1 = p1 )
let q1 be Element of L1; ::_thesis: ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 )
a = a "/\" [q1, the Element of L2] by A4
.= [(p1 "/\" q1),(p2 "/\" the Element of L2)] by A5, Th21 ;
hence ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 ) by A5, XTUPLE_0:1; ::_thesis: verum
end;
set q1 = the Element of L1;
take p2 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L2 holds
( p2 "/\" b1 = p2 & b1 "/\" p2 = p2 )
let q2 be Element of L2; ::_thesis: ( p2 "/\" q2 = p2 & q2 "/\" p2 = p2 )
a = a "/\" [ the Element of L1,q2] by A4
.= [(p1 "/\" the Element of L1),(p2 "/\" q2)] by A5, Th21 ;
hence ( p2 "/\" q2 = p2 & q2 "/\" p2 = p2 ) by A5, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th40: :: FILTER_1:40
for L1, L2 being Lattice holds
( ( L1 is upper-bounded & L2 is upper-bounded ) iff [:L1,L2:] is upper-bounded )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is upper-bounded & L2 is upper-bounded ) iff [:L1,L2:] is upper-bounded )
thus ( L1 is upper-bounded & L2 is upper-bounded implies [:L1,L2:] is upper-bounded ) ::_thesis: ( [:L1,L2:] is upper-bounded implies ( L1 is upper-bounded & L2 is upper-bounded ) )
proof
given p1 being Element of L1 such that A1: for q1 being Element of L1 holds
( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 ) ; :: according to LATTICES:def_14 ::_thesis: ( not L2 is upper-bounded or [:L1,L2:] is upper-bounded )
given p2 being Element of L2 such that A2: for q2 being Element of L2 holds
( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 ) ; :: according to LATTICES:def_14 ::_thesis: [:L1,L2:] is upper-bounded
take a = [p1,p2]; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of [:L1,L2:] holds
( a "\/" b1 = a & b1 "\/" a = a )
let b be Element of [:L1,L2:]; ::_thesis: ( a "\/" b = a & b "\/" a = a )
consider q1 being Element of L1, q2 being Element of L2 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 ; ::_thesis: b "\/" a = a
hence b "\/" a = a ; ::_thesis: verum
end;
given a being Element of [:L1,L2:] such that A4: for b being Element of [:L1,L2:] holds
( a "\/" b = a & b "\/" a = a ) ; :: according to LATTICES:def_14 ::_thesis: ( L1 is upper-bounded & L2 is upper-bounded )
consider p1 being Element of L1, p2 being Element of L2 such that
A5: a = [p1,p2] by DOMAIN_1:1;
thus L1 is upper-bounded ::_thesis: L2 is upper-bounded
proof
set q2 = the Element of L2;
take p1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L1 holds
( p1 "\/" b1 = p1 & b1 "\/" p1 = p1 )
let q1 be Element of L1; ::_thesis: ( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 )
a = a "\/" [q1, the Element of L2] by A4
.= [(p1 "\/" q1),(p2 "\/" the Element of L2)] by A5, Th21 ;
hence ( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 ) by A5, XTUPLE_0:1; ::_thesis: verum
end;
set q1 = the Element of L1;
take p2 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L2 holds
( p2 "\/" b1 = p2 & b1 "\/" p2 = p2 )
let q2 be Element of L2; ::_thesis: ( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 )
a = a "\/" [ the Element of L1,q2] by A4
.= [(p1 "\/" the Element of L1),(p2 "\/" q2)] by A5, Th21 ;
hence ( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 ) by A5, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th41: :: FILTER_1:41
for L1, L2 being Lattice holds
( ( L1 is bounded & L2 is bounded ) iff [:L1,L2:] is bounded )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is bounded & L2 is bounded ) iff [:L1,L2:] is bounded )
thus ( L1 is bounded & L2 is bounded implies [:L1,L2:] is bounded ) ::_thesis: ( [:L1,L2:] is bounded implies ( L1 is bounded & L2 is bounded ) )
proof
assume that
A1: L1 is lower-bounded and
A2: L1 is upper-bounded and
A3: L2 is lower-bounded and
A4: L2 is upper-bounded ; :: according to LATTICES:def_15 ::_thesis: [:L1,L2:] is bounded
thus ( [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded ) by A1, A2, A3, A4, Th39, Th40; :: according to LATTICES:def_15 ::_thesis: verum
end;
assume that
A5: [:L1,L2:] is lower-bounded and
A6: [:L1,L2:] is upper-bounded ; :: according to LATTICES:def_15 ::_thesis: ( L1 is bounded & L2 is bounded )
thus ( L1 is lower-bounded & L1 is upper-bounded & L2 is lower-bounded & L2 is upper-bounded ) by A5, A6, Th39, Th40; :: according to LATTICES:def_15 ::_thesis: verum
end;
theorem Th42: :: FILTER_1:42
for L1, L2 being Lattice st L1 is 0_Lattice & L2 is 0_Lattice holds
Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]
proof
let L1, L2 be Lattice; ::_thesis: ( L1 is 0_Lattice & L2 is 0_Lattice implies Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)] )
assume that
A1: L1 is 0_Lattice and
A2: L2 is 0_Lattice ; ::_thesis: Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]
A3: now__::_thesis:_for_a_being_Element_of_[:L1,L2:]_holds_
(_[(Bottom_L1),(Bottom_L2)]_"/\"_a_=_[(Bottom_L1),(Bottom_L2)]_&_a_"/\"_[(Bottom_L1),(Bottom_L2)]_=_[(Bottom_L1),(Bottom_L2)]_)
let a be Element of [:L1,L2:]; ::_thesis: ( [(Bottom L1),(Bottom L2)] "/\" a = [(Bottom L1),(Bottom L2)] & a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] )
consider p1 being Element of L1, p2 being Element of L2 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 ; ::_thesis: a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)]
hence a "/\" [(Bottom L1),(Bottom L2)] = [(Bottom L1),(Bottom L2)] ; ::_thesis: verum
end;
[:L1,L2:] is lower-bounded by A1, A2, Th39;
hence Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)] by A3, LATTICES:def_16; ::_thesis: verum
end;
theorem Th43: :: FILTER_1:43
for L1, L2 being Lattice st L1 is 1_Lattice & L2 is 1_Lattice holds
Top [:L1,L2:] = [(Top L1),(Top L2)]
proof
let L1, L2 be Lattice; ::_thesis: ( L1 is 1_Lattice & L2 is 1_Lattice implies Top [:L1,L2:] = [(Top L1),(Top L2)] )
assume that
A1: L1 is 1_Lattice and
A2: L2 is 1_Lattice ; ::_thesis: Top [:L1,L2:] = [(Top L1),(Top L2)]
A3: now__::_thesis:_for_a_being_Element_of_[:L1,L2:]_holds_
(_[(Top_L1),(Top_L2)]_"\/"_a_=_[(Top_L1),(Top_L2)]_&_a_"\/"_[(Top_L1),(Top_L2)]_=_[(Top_L1),(Top_L2)]_)
let a be Element of [:L1,L2:]; ::_thesis: ( [(Top L1),(Top L2)] "\/" a = [(Top L1),(Top L2)] & a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)] )
consider p1 being Element of L1, p2 being Element of L2 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 ; ::_thesis: a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)]
hence a "\/" [(Top L1),(Top L2)] = [(Top L1),(Top L2)] ; ::_thesis: verum
end;
[:L1,L2:] is upper-bounded by A1, A2, Th40;
hence Top [:L1,L2:] = [(Top L1),(Top L2)] by A3, LATTICES:def_17; ::_thesis: verum
end;
theorem Th44: :: FILTER_1:44
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
proof
let L1, L2 be Lattice; ::_thesis: for p1, q1 being Element of L1
for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
let p1, q1 be Element of L1; ::_thesis: for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
let p2, q2 be Element of L2; ::_thesis: ( 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] ) )
assume that
A1: L1 is 01_Lattice and
A2: L2 is 01_Lattice ; ::_thesis: ( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
thus ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 implies [p1,p2] is_a_complement_of [q1,q2] ) ::_thesis: ( [p1,p2] is_a_complement_of [q1,q2] implies ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) )
proof
assume that
A3: p1 is_a_complement_of q1 and
A4: p2 is_a_complement_of q2 ; ::_thesis: [p1,p2] is_a_complement_of [q1,q2]
A5: p2 "\/" q2 = Top L2 by A4, LATTICES:def_18;
p1 "\/" q1 = Top L1 by A3, LATTICES:def_18;
hence [p1,p2] "\/" [q1,q2] = [(Top L1),(Top L2)] by A5, Th21
.= Top [:L1,L2:] by A1, A2, Th43 ;
:: according to LATTICES:def_18 ::_thesis: ( [q1,q2] "\/" [p1,p2] = Top [:L1,L2:] & [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] & [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] )
hence [q1,q2] "\/" [p1,p2] = Top [:L1,L2:] ; ::_thesis: ( [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] & [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] )
A6: p2 "/\" q2 = Bottom L2 by A4, LATTICES:def_18;
p1 "/\" q1 = Bottom L1 by A3, LATTICES:def_18;
hence [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A6, Th21
.= Bottom [:L1,L2:] by A1, A2, Th42 ;
::_thesis: [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:]
hence [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] ; ::_thesis: verum
end;
assume A7: [p1,p2] is_a_complement_of [q1,q2] ; ::_thesis: ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 )
then A8: [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] by LATTICES:def_18;
[(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, LATTICES:def_18;
A12: p2 "/\" q2 = Bottom L2 by A9, XTUPLE_0:1;
[(Top L1),(Top L2)] = Top [:L1,L2:] by A1, A2, Th43;
then A13: [(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, LATTICES:def_18; ::_thesis: p2 is_a_complement_of q2
p2 "\/" q2 = Top L2 by A13, XTUPLE_0:1;
hence p2 is_a_complement_of q2 by A12, LATTICES:def_18; ::_thesis: verum
end;
theorem Th45: :: FILTER_1:45
for L1, L2 being Lattice holds
( ( L1 is C_Lattice & L2 is C_Lattice ) iff [:L1,L2:] is C_Lattice )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is C_Lattice & L2 is C_Lattice ) iff [:L1,L2:] is C_Lattice )
thus ( L1 is C_Lattice & L2 is C_Lattice implies [:L1,L2:] is C_Lattice ) ::_thesis: ( [:L1,L2:] is C_Lattice implies ( L1 is C_Lattice & L2 is C_Lattice ) )
proof
assume that
A1: L1 is C_Lattice and
A2: L2 is C_Lattice ; ::_thesis: [:L1,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; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of a
consider p1 being Element of L1, p2 being Element of L2 such that
A3: a = [p1,p2] by DOMAIN_1:1;
consider q1 being Element of L1 such that
A4: q1 is_a_complement_of p1 by A1, LATTICES:def_19;
consider q2 being Element of L2 such that
A5: q2 is_a_complement_of p2 by A2, LATTICES:def_19;
reconsider b = [q1,q2] as Element of L ;
take b ; ::_thesis: b is_a_complement_of a
thus b is_a_complement_of a by A1, A2, A3, A4, A5, Th44; ::_thesis: verum
end;
hence [:L1,L2:] is C_Lattice ; ::_thesis: verum
end;
assume A6: [:L1,L2:] is C_Lattice ; ::_thesis: ( L1 is C_Lattice & 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; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of C1 st b1 is_a_complement_of p19
reconsider p1 = p19 as Element of L1 ;
reconsider p2 = the Element of C2 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 being Element of L1, q2 being Element of L2 such that
A8: b = [q1,q2] by DOMAIN_1:1;
reconsider q19 = q1 as Element of C1 ;
take q19 ; ::_thesis: q19 is_a_complement_of p19
thus q19 is_a_complement_of p19 by A7, A8, Th44; ::_thesis: verum
end;
hence L1 is C_Lattice ; ::_thesis: L2 is C_Lattice
C2 is complemented
proof
set p19 = the Element of C1;
let p29 be Element of C2; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of C2 st b1 is_a_complement_of p29
reconsider p1 = the Element of C1 as Element of L1 ;
reconsider p2 = p29 as Element of L2 ;
consider b being Element of [:L1,L2:] such that
A9: b is_a_complement_of [p1,p2] by A6, LATTICES:def_19;
consider q1 being Element of L1, q2 being Element of L2 such that
A10: b = [q1,q2] by DOMAIN_1:1;
reconsider q29 = q2 as Element of C2 ;
take q29 ; ::_thesis: q29 is_a_complement_of p29
thus q29 is_a_complement_of p29 by A9, A10, Th44; ::_thesis: verum
end;
hence L2 is C_Lattice ; ::_thesis: verum
end;
theorem :: FILTER_1:46
for L1, L2 being Lattice holds
( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )
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 ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice ) by A1; ::_thesis: verum
end;
theorem :: FILTER_1:47
for L1, L2 being Lattice holds
( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )
proof
let L1, L2 be Lattice; ::_thesis: ( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )
thus ( L1 is implicative & L2 is implicative implies [:L1,L2:] is implicative ) ::_thesis: ( [:L1,L2:] is implicative implies ( L1 is implicative & L2 is implicative ) )
proof
assume A1: for p1, q1 being Element of L1 ex r1 being Element of L1 st
( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 ) ) ; :: according to FILTER_0:def_6 ::_thesis: ( not L2 is implicative or [:L1,L2:] is implicative )
assume A2: for p2, q2 being Element of L2 ex r2 being Element of L2 st
( p2 "/\" r2 [= q2 & ( for s2 being Element of L2 st p2 "/\" s2 [= q2 holds
s2 [= r2 ) ) ; :: according to FILTER_0:def_6 ::_thesis: [:L1,L2:] is implicative
let a, b be Element of [:L1,L2:]; :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of [:L1,L2:] st
( a "/\" b1 [= b & ( for b2 being Element of the carrier of [:L1,L2:] holds
( not a "/\" b2 [= b or b2 [= b1 ) ) )
consider p1 being Element of L1, p2 being Element of L2 such that
A3: a = [p1,p2] by DOMAIN_1:1;
consider q1 being Element of L1, q2 being Element of L2 such that
A4: b = [q1,q2] by DOMAIN_1:1;
consider r2 being Element of L2 such that
A5: p2 "/\" r2 [= q2 and
A6: for s2 being Element of L2 st p2 "/\" s2 [= q2 holds
s2 [= r2 by A2;
consider r1 being Element of L1 such that
A7: p1 "/\" r1 [= q1 and
A8: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 by A1;
take [r1,r2] ; ::_thesis: ( a "/\" [r1,r2] [= b & ( for b1 being Element of the carrier of [:L1,L2:] holds
( not a "/\" b1 [= b or b1 [= [r1,r2] ) ) )
a "/\" [r1,r2] = [(p1 "/\" r1),(p2 "/\" r2)] by A3, Th21;
hence a "/\" [r1,r2] [= b by A4, A7, A5, Th36; ::_thesis: for b1 being Element of the carrier of [:L1,L2:] holds
( not a "/\" b1 [= b or b1 [= [r1,r2] )
let d be Element of [:L1,L2:]; ::_thesis: ( not a "/\" d [= b or d [= [r1,r2] )
consider s1 being Element of L1, s2 being Element of L2 such that
A9: d = [s1,s2] by DOMAIN_1:1;
assume a "/\" d [= b ; ::_thesis: d [= [r1,r2]
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; ::_thesis: verum
end;
assume A12: for a, b being Element of [:L1,L2:] ex c being Element of [:L1,L2:] st
( a "/\" c [= b & ( for d being Element of [:L1,L2:] st a "/\" d [= b holds
d [= c ) ) ; :: according to FILTER_0:def_6 ::_thesis: ( L1 is implicative & L2 is implicative )
thus for p1, q1 being Element of L1 ex r1 being Element of L1 st
( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 ) ) :: according to FILTER_0:def_6 ::_thesis: L2 is implicative
proof
set p2 = the Element of L2;
let p1, q1 be Element of L1; ::_thesis: ex r1 being Element of L1 st
( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 ) )
consider c being Element of [:L1,L2:] such that
A13: [p1, the Element of L2] "/\" c [= [q1, the Element of L2] and
A14: for d being Element of [:L1,L2:] st [p1, the Element of L2] "/\" d [= [q1, the Element of L2] holds
d [= c by A12;
consider r1 being Element of L1, r2 being Element of L2 such that
A15: c = [r1,r2] by DOMAIN_1:1;
take r1 ; ::_thesis: ( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 ) )
A16: [p1, the Element of L2] "/\" c = [(p1 "/\" r1),( the Element of L2 "/\" r2)] by A15, Th21;
hence p1 "/\" r1 [= q1 by A13, Th36; ::_thesis: for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1
let s1 be Element of L1; ::_thesis: ( p1 "/\" s1 [= q1 implies s1 [= r1 )
assume A17: p1 "/\" s1 [= q1 ; ::_thesis: s1 [= r1
the Element of L2 "/\" r2 [= the Element of L2 by A13, A16, Th36;
then [(p1 "/\" s1),( the Element of L2 "/\" r2)] [= [q1, the Element of L2] by A17, Th36;
then [p1, the Element of L2] "/\" [s1,r2] [= [q1, the Element of L2] by Th21;
then [s1,r2] [= c by A14;
hence s1 [= r1 by A15, Th36; ::_thesis: verum
end;
set p1 = the Element of L1;
let p2 be Element of L2; :: according to FILTER_0:def_6 ::_thesis: for b1 being Element of the carrier of L2 ex b2 being Element of the carrier of L2 st
( p2 "/\" b2 [= b1 & ( for b3 being Element of the carrier of L2 holds
( not p2 "/\" b3 [= b1 or b3 [= b2 ) ) )
let q2 be Element of L2; ::_thesis: ex b1 being Element of the carrier of L2 st
( p2 "/\" b1 [= q2 & ( for b2 being Element of the carrier of L2 holds
( not p2 "/\" b2 [= q2 or b2 [= b1 ) ) )
consider c being Element of [:L1,L2:] such that
A18: [ the Element of L1,p2] "/\" c [= [ the Element of L1,q2] and
A19: for d being Element of [:L1,L2:] st [ the Element of L1,p2] "/\" d [= [ the Element of L1,q2] holds
d [= c by A12;
consider r1 being Element of L1, r2 being Element of L2 such that
A20: c = [r1,r2] by DOMAIN_1:1;
take r2 ; ::_thesis: ( p2 "/\" r2 [= q2 & ( for b1 being Element of the carrier of L2 holds
( not p2 "/\" b1 [= q2 or b1 [= r2 ) ) )
A21: [ the Element of L1,p2] "/\" c = [( the Element of L1 "/\" r1),(p2 "/\" r2)] by A20, Th21;
hence p2 "/\" r2 [= q2 by A18, Th36; ::_thesis: for b1 being Element of the carrier of L2 holds
( not p2 "/\" b1 [= q2 or b1 [= r2 )
let s2 be Element of L2; ::_thesis: ( not p2 "/\" s2 [= q2 or s2 [= r2 )
assume A22: p2 "/\" s2 [= q2 ; ::_thesis: s2 [= r2
the Element of L1 "/\" r1 [= the Element of L1 by A18, A21, Th36;
then [( the Element of L1 "/\" r1),(p2 "/\" s2)] [= [ the Element of L1,q2] by A22, Th36;
then [ the Element of L1,p2] "/\" [r1,s2] [= [ the Element of L1,q2] by Th21;
then [r1,s2] [= c by A19;
hence s2 [= r2 by A20, Th36; ::_thesis: verum
end;
theorem :: FILTER_1:48
for L1, L2 being Lattice holds [:L1,L2:] .: = [:(L1 .:),(L2 .:):] ;
theorem :: FILTER_1:49
for L1, L2 being Lattice holds [:L1,L2:],[:L2,L1:] are_isomorphic
proof
let L1, L2 be Lattice; ::_thesis: [:L1,L2:],[:L2,L1:] are_isomorphic
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 ( the carrier of L1, the carrier of L2);
set p1 = pr1 ( the carrier of L1, the carrier of L2);
take f = <:(pr2 ( the carrier of L1, the carrier of L2)),(pr1 ( the carrier of L1, the carrier of L2)):>; :: according to WELLORD1:def_8,FILTER_1:def_9 ::_thesis: f is_isomorphism_of LattRel [:L1,L2:], LattRel [:L2,L1:]
A1: dom (pr2 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def_5;
A2: field (LattRel [:L1,L2:]) = the carrier of [:L1,L2:] by Th32;
A3: rng (pr2 ( the carrier of L1, the carrier of L2)) = the carrier of L2 by FUNCT_3:46;
A4: field (LattRel [:L2,L1:]) = the carrier of [:L2,L1:] by Th32;
dom (pr1 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def_4;
then (dom (pr2 ( the carrier of L1, the carrier of L2))) /\ (dom (pr1 ( the carrier of L1, the carrier of L2))) = [: the carrier of L1, the carrier of L2:] by A1;
hence A5: dom f = field (LattRel [:L1,L2:]) by A2, FUNCT_3:def_7; :: according to WELLORD1:def_7 ::_thesis: ( rng f = field (LattRel [:L2,L1:]) & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
rng (pr1 ( the carrier of L1, the carrier of L2)) = the carrier of L1 by FUNCT_3:44;
hence rng f c= field (LattRel [:L2,L1:]) by A4, A3, FUNCT_3:51; :: according to XBOOLE_0:def_10 ::_thesis: ( field (LattRel [:L2,L1:]) c= rng f & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
thus field (LattRel [:L2,L1:]) c= rng f ::_thesis: ( f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field (LattRel [:L2,L1:]) or x in rng f )
assume x in field (LattRel [:L2,L1:]) ; ::_thesis: x in rng f
then consider r2 being Element of L2, r1 being Element of L1 such that
A6: x = [r2,r1] by A4, DOMAIN_1:1;
A7: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def_5;
A8: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def_4;
f . [r1,r2] in rng f by A2, A5, FUNCT_1:def_3;
hence x in rng f by A2, A5, A6, A7, A8, FUNCT_3:def_7; ::_thesis: verum
end;
thus f is one-to-one ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A9: x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y )
then A10: f . x = [((pr2 ( the carrier of L1, the carrier of L2)) . x),((pr1 ( the carrier of L1, the carrier of L2)) . x)] by FUNCT_3:def_7;
consider r1 being Element of L1, r2 being Element of L2 such that
A11: x = [r1,r2] by A2, A5, A9, DOMAIN_1:1;
A12: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def_5;
A13: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def_4;
assume that
A14: y in dom f and
A15: f . x = f . y ; ::_thesis: x = y
A16: f . y = [((pr2 ( the carrier of L1, the carrier of L2)) . y),((pr1 ( the carrier of L1, the carrier of L2)) . y)] by A14, FUNCT_3:def_7;
consider q1 being Element of L1, q2 being Element of L2 such that
A17: y = [q1,q2] by A2, A5, A14, DOMAIN_1:1;
A18: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def_5;
(pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def_4;
then r1 = q1 by A11, A15, A17, A13, A10, A16, XTUPLE_0:1;
hence x = y by A11, A15, A17, A12, A18, A10, A16, XTUPLE_0:1; ::_thesis: verum
end;
let x, y be set ; ::_thesis: ( ( not [x,y] in LattRel [:L1,L2:] or ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) & ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] ) )
thus ( [x,y] in LattRel [:L1,L2:] implies ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) ::_thesis: ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )
proof
assume [x,y] in LattRel [:L1,L2:] ; ::_thesis: ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] )
then consider a, b being Element of [:L1,L2:] such that
A19: [x,y] = [a,b] and
A20: a [= b ;
consider q1 being Element of L1, q2 being Element of L2 such that
A21: b = [q1,q2] by DOMAIN_1:1;
A22: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A21, FUNCT_3:def_7;
A23: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def_5;
consider r1 being Element of L1, r2 being Element of L2 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: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def_4;
A28: (pr2 ( the carrier of L1, the carrier of L2)) . (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 (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) ) by A2, A29; ::_thesis: [(f . x),(f . y)] in LattRel [:L2,L1:]
A31: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def_4;
f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A24, FUNCT_3:def_7;
hence [(f . x),(f . y)] in LattRel [:L2,L1:] by A24, A21, A30, A29, A26, A27, A28, A31, A23, A22; ::_thesis: verum
end;
assume that
A32: x in field (LattRel [:L1,L2:]) and
A33: y in field (LattRel [:L1,L2:]) ; ::_thesis: ( not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )
consider q1 being Element of L1, q2 being Element of L2 such that
A34: y = [q1,q2] by A2, A33, DOMAIN_1:1;
A35: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A34, FUNCT_3:def_7;
assume A36: [(f . x),(f . y)] in LattRel [:L2,L1:] ; ::_thesis: [x,y] in LattRel [:L1,L2:]
A37: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def_5;
A38: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def_4;
consider r1 being Element of L1, r2 being Element of L2 such that
A39: x = [r1,r2] by A2, A32, DOMAIN_1:1;
A40: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def_5;
A41: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def_4;
f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (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 [x,y] in LattRel [:L1,L2:] by A39, A34; ::_thesis: verum
end;
theorem Th50: :: FILTER_1:50
for B being B_Lattice
for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
let a, b be Element of B; ::_thesis: a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
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 `)) ; ::_thesis: verum
end;
theorem Th51: :: FILTER_1:51
for B being B_Lattice
for a, b being Element of B holds
( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds
( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
let a, b be Element of B; ::_thesis: ( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
A1: now__::_thesis:_for_a,_b_being_Element_of_B_holds_(a_=>_b)_`_=_a_"/\"_(b_`)
let a, b be Element of B; ::_thesis: (a => b) ` = a "/\" (b `)
thus (a => b) ` = ((a `) "\/" b) ` by FILTER_0:42
.= ((a `) `) "/\" (b `) by LATTICES:24
.= a "/\" (b `) ; ::_thesis: verum
end;
hence (a => b) ` = a "/\" (b `) ; ::_thesis: ( (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (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 ; ::_thesis: ( (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
hence (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" ((b `) `))
.= a <=> (b `) by Th50 ;
::_thesis: (a <=> b) ` = (a `) <=> b
hence (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" ((b `) `)) by Th50
.= (((a `) `) "/\" (b `)) "\/" ((a `) "/\" ((b `) `))
.= ((a `) "/\" b) "\/" (((a `) `) "/\" (b `))
.= (a `) <=> b by Th50 ;
::_thesis: verum
end;
theorem Th52: :: FILTER_1:52
for B being B_Lattice
for a, b, c being Element of B st a <=> b = a <=> c holds
b = c
proof
let B be B_Lattice; ::_thesis: for a, b, c being Element of B st a <=> b = a <=> c holds
b = c
let a, b, c be Element of B; ::_thesis: ( a <=> b = a <=> c implies b = c )
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;
B1: ( a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `)) & a <=> c = (a "/\" c) "\/" ((a `) "/\" (c `)) ) by Th50;
C1: (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) by Th51;
D1: (a <=> c) ` = (a "/\" (c `)) "\/" ((a `) "/\" c) by Th51;
E1: ((a "/\" b) "\/" ((a `) "/\" (b `))) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = ((a "/\" b) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `)))) "\/" (((a `) "/\" (b `)) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `)))) by LATTICES:def_11;
F1: ( (a "/\" b) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = ((a "/\" b) "/\" (a "/\" c)) "\/" ((a "/\" b) "/\" ((a `) "/\" (c `))) & (a "/\" b) "/\" ((a `) "/\" (c `)) = ((a "/\" b) "/\" (a `)) "/\" (c `) ) by LATTICES:def_7, LATTICES:def_11;
G1: ((a `) "/\" (b `)) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = (((a `) "/\" (b `)) "/\" (a "/\" c)) "\/" (((a `) "/\" (b `)) "/\" ((a `) "/\" (c `))) by LATTICES:def_11;
H1: (b "/\" a) "/\" (a `) = b "/\" (a "/\" (a `)) by LATTICES:def_7;
L1: (b `) "/\" (Bottom B) = Bottom B ;
R1: ((a `) "/\" (b `)) "/\" (a "/\" c) = (((a `) "/\" (b `)) "/\" a) "/\" c by LATTICES:def_7;
S1: ((b `) "/\" (a `)) "/\" a = (b `) "/\" ((a `) "/\" a) by LATTICES:def_7;
T1: ((a "/\" b) "/\" (a "/\" c)) "\/" (Bottom B) = (a "/\" b) "/\" (a "/\" c) ;
U1: (Bottom B) "\/" (((a `) "/\" (b `)) "/\" ((a `) "/\" (c `))) = ((a `) "/\" (b `)) "/\" ((a `) "/\" (c `)) ;
V1: ((a "/\" (b `)) "\/" ((a `) "/\" b)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = ((a "/\" (b `)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c))) "\/" (((a `) "/\" b) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c))) by LATTICES:def_11;
X1: ( (a "/\" (b `)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = ((a "/\" (b `)) "/\" (a "/\" (c `))) "\/" ((a "/\" (b `)) "/\" ((a `) "/\" c)) & (a "/\" (b `)) "/\" ((a `) "/\" c) = ((a "/\" (b `)) "/\" (a `)) "/\" c ) by LATTICES:def_7, LATTICES:def_11;
Y1: ((a `) "/\" b) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = (((a `) "/\" b) "/\" (a "/\" (c `))) "\/" (((a `) "/\" b) "/\" ((a `) "/\" c)) by LATTICES:def_11;
I1: ((b `) "/\" a) "/\" (a `) = (b `) "/\" (a "/\" (a `)) by LATTICES:def_7;
J1: ( b "/\" (Bottom B) = Bottom B & (Bottom B) "/\" (c `) = Bottom B & (Bottom B) "/\" c = Bottom B & a "/\" (a `) = Bottom B & (a `) "/\" a = Bottom B & a "/\" (b `) = (b `) "/\" a & (a `) "/\" b = b "/\" (a `) & ((a `) "/\" b) "/\" (a "/\" (c `)) = (((a `) "/\" b) "/\" a) "/\" (c `) & (b "/\" (a `)) "/\" a = b "/\" ((a `) "/\" a) & ((a "/\" (b `)) "/\" (a "/\" (c `))) "\/" (Bottom B) = (a "/\" (b `)) "/\" (a "/\" (c `)) & (Bottom B) "\/" (((a `) "/\" b) "/\" ((a `) "/\" c)) = ((a `) "/\" b) "/\" ((a `) "/\" c) ) by LATTICES:20, LATTICES:def_7;
( (a "/\" b) "/\" (a "/\" c) = ((a "/\" b) "/\" a) "/\" c & (a "/\" b) "/\" a = a "/\" (a "/\" b) & a "/\" (a "/\" b) = (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 ` & (a "/\" (b `)) "/\" (a "/\" (c `)) = ((a "/\" (b `)) "/\" a) "/\" (c `) & (a "/\" (b `)) "/\" a = a "/\" (a "/\" (b `)) & (a "/\" b) "/\" c = a "/\" (b "/\" c) & a "/\" (a "/\" (b `)) = (a "/\" a) "/\" (b `) & ((a `) "/\" b) "/\" ((a `) "/\" c) = (((a `) "/\" b) "/\" (a `)) "/\" c & ((a `) "/\" b) "/\" (a `) = (a `) "/\" ((a `) "/\" b) & ((a `) "/\" b) "/\" c = (a `) "/\" (b "/\" c) & (a "/\" (b `)) "/\" (c `) = a "/\" ((b `) "/\" (c `)) & ((a `) "/\" (b `)) "/\" (c `) = (a `) "/\" ((b `) "/\" (c `)) & (a `) "/\" ((a `) "/\" b) = ((a `) "/\" (a `)) "/\" b & ((a "/\" (b "/\" c)) "\/" ((a `) "/\" ((b `) "/\" (c `)))) "\/" ((a "/\" ((b `) "/\" (c `))) "\/" ((a `) "/\" (b "/\" c))) = (((a "/\" (b "/\" c)) "\/" ((a `) "/\" ((b `) "/\" (c `)))) "\/" (a "/\" ((b `) "/\" (c `)))) "\/" ((a `) "/\" (b "/\" c)) & ((a "/\" (b "/\" c)) "\/" ((a `) "/\" ((b `) "/\" (c `)))) "\/" (a "/\" ((b `) "/\" (c `))) = (a "/\" ((b `) "/\" (c `))) "\/" ((a "/\" (b "/\" c)) "\/" ((a `) "/\" ((b `) "/\" (c `)))) & (a "/\" ((b `) "/\" (c `))) "\/" ((a "/\" (b "/\" c)) "\/" ((a `) "/\" ((b `) "/\" (c `)))) = ((a "/\" ((b `) "/\" (c `))) "\/" (a "/\" (b "/\" c))) "\/" ((a `) "/\" ((b `) "/\" (c `))) & (a "/\" ((b `) "/\" (c `))) "\/" (a "/\" (b "/\" c)) = a "/\" (((b `) "/\" (c `)) "\/" (b "/\" c)) & ((b `) "/\" (c `)) "\/" (b "/\" c) = (b "/\" c) "\/" ((b `) "/\" (c `)) & ((a `) "/\" ((b `) "/\" (c `))) "\/" ((a `) "/\" (b "/\" c)) = (a `) "/\" (((b `) "/\" (c `)) "\/" (b "/\" c)) & (Top B) "/\" (((b `) "/\" (c `)) "\/" (b "/\" c)) = ((b `) "/\" (c `)) "\/" (b "/\" c) & ((a "/\" (((b `) "/\" (c `)) "\/" (b "/\" c))) "\/" ((a `) "/\" ((b `) "/\" (c `)))) "\/" ((a `) "/\" (b "/\" c)) = (a "/\" (((b `) "/\" (c `)) "\/" (b "/\" c))) "\/" (((a `) "/\" ((b `) "/\" (c `))) "\/" ((a `) "/\" (b "/\" c))) & a "\/" (a `) = Top B & (a "/\" (((b `) "/\" (c `)) "\/" (b "/\" c))) "\/" ((a `) "/\" (((b `) "/\" (c `)) "\/" (b "/\" c))) = (a "\/" (a `)) "/\" (((b `) "/\" (c `)) "\/" (b "/\" c)) ) by LATTICES:21, LATTICES:def_5, LATTICES:def_7, LATTICES:def_11;
then A2: (a <=> b) <=> (a <=> c) = b <=> c by B1, A1, Th50, C1, D1, E1, F1, G1, H1, I1, J1, L1, R1, S1, T1, U1, V1, X1, Y1;
assume A3: a <=> b = a <=> c ; ::_thesis: b = c
then B4: (a <=> b) => (a <=> c) = Top B by FILTER_0:28;
((a <=> b) => (a <=> b)) "/\" ((a <=> b) => (a <=> b)) = (a <=> b) => (a <=> b) ;
then A4: b <=> c = Top B by A2, A3, B4;
then A5: b "/\" (Top B) [= b "/\" (b => c) by LATTICES:6, LATTICES:9;
A6: c "/\" (Top B) [= c "/\" (c => b) by A4, LATTICES:6, LATTICES:9;
A7: b "/\" (b => c) [= c by FILTER_0:def_7;
A8: c "/\" (c => b) [= b by FILTER_0:def_7;
A11: b [= c by A5, A7, LATTICES:7;
c [= b by A6, A8, LATTICES:7;
hence b = c by A11, LATTICES:8; ::_thesis: verum
end;
theorem Th53: :: FILTER_1:53
for B being B_Lattice
for a, b being Element of B holds a <=> (a <=> b) = b
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds a <=> (a <=> b) = b
let a, b be Element of B; ::_thesis: a <=> (a <=> b) = b
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;
A5: (Bottom B) "/\" (b `) = Bottom B ;
A6: a "\/" (a `) = Top B by LATTICES:21;
A7: (a "/\" b) "\/" ((a `) "/\" b) = (a "\/" (a `)) "/\" b by LATTICES:def_11;
A8: (Bottom B) "\/" ((a `) "/\" b) = (a `) "/\" b ;
A9: (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) by Th51;
A10: (a `) "/\" (a "/\" (b `)) = ((a `) "/\" a) "/\" (b `) by LATTICES:def_7;
A11: (a "/\" b) "\/" (Bottom B) = a "/\" b ;
A12: a "/\" (a `) = Bottom B by LATTICES:20;
A13: a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `)) by Th50;
A14: a "/\" (a "/\" b) = (a "/\" a) "/\" b by LATTICES:def_7;
A15: a "/\" ((a `) "/\" (b `)) = (a "/\" (a `)) "/\" (b `) by LATTICES:def_7;
A16: (a `) "/\" ((a `) "/\" b) = ((a `) "/\" (a `)) "/\" b by LATTICES:def_7;
a <=> (a <=> b) = (a "/\" (a <=> b)) "\/" ((a `) "/\" ((a <=> b) `)) by Th50;
hence a <=> (a <=> b) = b by A13, A9, A1, A2, A14, A10, A16, A15, A12, A11, A8, A7, A6, A5, LATTICES:17; ::_thesis: verum
end;
theorem :: FILTER_1:54
for I being I_Lattice
for i, j being Element of I holds
( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
proof
let I be I_Lattice; ::_thesis: for i, j being Element of I holds
( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
let i, j be Element of I; ::_thesis: ( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
A1: i "\/" i = i ;
j "/\" (j => i) [= i by FILTER_0:def_7;
then A2: i "\/" (j "/\" (j => i)) [= i by A1, FILTER_0:1;
A3: (i "\/" j) "/\" (j => i) [= (i "\/" j) "/\" (i "\/" (j => i)) by LATTICES:5, LATTICES:9;
A4: 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 A4, LATTICES:7;
then A5: (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 A2, A3, LATTICES:7;
then j => i [= (i "\/" j) => i by FILTER_0:def_7;
hence (i "\/" j) => i = j => i by A5, LATTICES:8; ::_thesis: i => (i "/\" j) = i => j
A6: j "/\" i [= j by LATTICES:6;
i "/\" (i => (i "/\" j)) [= i "/\" j by FILTER_0:def_7;
then i "/\" (i => (i "/\" j)) [= j by A6, LATTICES:7;
then A7: i => (i "/\" j) [= i => j by FILTER_0:def_7;
i "/\" (i => j) [= j by FILTER_0:def_7;
then A9: 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 A9, FILTER_0:def_7;
hence i => (i "/\" j) = i => j by A7, LATTICES:8; ::_thesis: verum
end;
theorem Th55: :: FILTER_1:55
for I being I_Lattice
for i, j, k being Element of I holds
( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I holds
( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
let i, j, k be Element of I; ::_thesis: ( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
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 ( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j ) by A2, FILTER_0:def_7; ::_thesis: verum
end;
Lm1: for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
let FI be Filter of I; ::_thesis: for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
let i, j, k be Element of I; ::_thesis: ( 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 ) )
A1: i => j [= (i "/\" k) => j by Th55;
i => j [= i => (j "\/" k) by Th55;
hence ( 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 ) ) by A1, FILTER_0:9; ::_thesis: verum
end;
theorem Th56: :: FILTER_1:56
for I being I_Lattice
for i, k, j being Element of I holds (i => k) "/\" (j => k) [= (i "\/" j) => k
proof
let I be I_Lattice; ::_thesis: for i, k, j being Element of I holds (i => k) "/\" (j => k) [= (i "\/" j) => k
let i, k, j be Element of I; ::_thesis: (i => k) "/\" (j => k) [= (i "\/" j) => k
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 (i => k) "/\" (j => k) [= (i "\/" j) => k by FILTER_0:def_7; ::_thesis: verum
end;
Lm2: for I being I_Lattice
for FI being Filter of I
for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
let FI be Filter of I; ::_thesis: for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
let i, k, j be Element of I; ::_thesis: ( i => k in FI & j => k in FI implies (i "\/" j) => k in FI )
assume that
A1: i => k in FI and
A2: j => k in FI ; ::_thesis: (i "\/" 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 (i "\/" j) => k in FI by A3, FILTER_0:9; ::_thesis: verum
end;
theorem Th57: :: FILTER_1:57
for I being I_Lattice
for i, j, k being Element of I holds (i => j) "/\" (i => k) [= i => (j "/\" k)
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I holds (i => j) "/\" (i => k) [= i => (j "/\" k)
let i, j, k be Element of I; ::_thesis: (i => j) "/\" (i => k) [= i => (j "/\" k)
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 (i => j) "/\" (i => k) [= i => (j "/\" k) by A2, A3, A5, A4, FILTER_0:def_7; ::_thesis: verum
end;
Lm3: for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI & i => k in FI holds
i => (j "/\" k) in FI
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, j, k being Element of I st i => j in FI & i => k in FI holds
i => (j "/\" k) in FI
let FI be Filter of I; ::_thesis: for i, j, k being Element of I st i => j in FI & i => k in FI holds
i => (j "/\" k) in FI
let i, j, k be Element of I; ::_thesis: ( i => j in FI & i => k in FI implies i => (j "/\" k) in FI )
assume that
A1: i => j in FI and
A2: i => k in FI ; ::_thesis: i => (j "/\" 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 i => (j "/\" k) in FI by A3, FILTER_0:9; ::_thesis: verum
end;
theorem Th58: :: FILTER_1:58
for I being I_Lattice
for FI being Filter of I
for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds
( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds
( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )
let FI be Filter of I; ::_thesis: for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds
( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )
let i1, i2, j1, j2 be Element of I; ::_thesis: ( i1 <=> i2 in FI & j1 <=> j2 in FI implies ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) )
assume that
A1: i1 <=> i2 in FI and
A2: j1 <=> j2 in FI ; ::_thesis: ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" 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 ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) by A11, A7, A13, FILTER_0:8; ::_thesis: verum
end;
Lm4: for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
let FI be Filter of I; ::_thesis: for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
let i, j be Element of I; ::_thesis: ( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
( i in Class ((equivalence_wrt FI),j) iff [i,j] in equivalence_wrt FI ) by EQREL_1:19;
hence ( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI ) by FILTER_0:def_11; ::_thesis: verum
end;
theorem Th59: :: FILTER_1:59
for I being I_Lattice
for FI being Filter of I
for i, k, j being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
proof
let I be I_Lattice; ::_thesis: for FI being Filter of I
for i, k, j being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
let FI be Filter of I; ::_thesis: for i, k, j being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
let i, k, j be Element of I; ::_thesis: ( 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) ) )
assume that
A1: i in Class ((equivalence_wrt FI),k) and
A2: j in Class ((equivalence_wrt FI),k) ; ::_thesis: ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" 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 ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) ) by A5, Lm4; ::_thesis: verum
end;
theorem Th60: :: FILTER_1:60
for B being B_Lattice
for c, d being Element of B holds
( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d) ) )
proof
let B be B_Lattice; ::_thesis: for c, d being Element of B holds
( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d) ) )
let c, d be Element of B; ::_thesis: ( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d) ) )
set A = Class ((equivalence_wrt <.d.)),c);
A1: c in Class ((equivalence_wrt <.d.)),c) 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 Class ((equivalence_wrt <.d.)),c) by A3, A2, Lm4;
hence c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) by A1, Th59; ::_thesis: for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d)
let b be Element of B; ::_thesis: ( b in Class ((equivalence_wrt <.d.)),c) implies b [= c "\/" (c <=> d) )
assume b in Class ((equivalence_wrt <.d.)),c) ; ::_thesis: b [= c "\/" (c <=> d)
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: (b "/\" (c `)) "\/" (Bottom B) = b "/\" (c `) ;
A9: ((c `) "/\" (d `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" c by FILTER_0:1, LATTICES:6;
A10: b "/\" (Top B) = b ;
A11: (b "/\" (c `)) "\/" (b "/\" c) = b "/\" ((c `) "\/" c) by LATTICES:def_11;
A12: (b `) "/\" (Bottom B) = Bottom B ;
A13: (c "\/" (c "/\" d)) "\/" ((c `) "/\" (d `)) = c "\/" ((c "/\" d) "\/" ((c `) "/\" (d `))) by LATTICES:def_5;
A14: c = c "\/" (c "/\" d) by LATTICES:def_8;
A15: (c "/\" d) "\/" ((c `) "/\" (d `)) = c <=> d by Th50;
A17: (c `) "\/" c = Top B by LATTICES:21;
A18: 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, A8, A7, A18, A12, FILTER_0:1;
hence b [= c "\/" (c <=> d) by A11, A17, A10, A9, A14, A15, A13, LATTICES:7; ::_thesis: verum
end;
theorem :: FILTER_1:61
for B being B_Lattice
for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
proof
let B be B_Lattice; ::_thesis: for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
let a be Element of B; ::_thesis: B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
set F = <.a.);
set E = equivalence_wrt <.a.);
deffunc H3( set ) -> Element of bool the carrier of B = Class ((equivalence_wrt <.a.)),$1);
consider g being Function such that
A1: ( dom g = the carrier of B & ( for x being set st x in the carrier of B holds
g . x = H3(x) ) ) from FUNCT_1:sch_3();
A2: for b being Element of B holds (b "\/" (b <=> a)) <=> b = b "\/" a
proof
let b be Element of B; ::_thesis: (b "\/" (b <=> a)) <=> b = b "\/" a
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: (Bottom B) "/\" (a `) = Bottom B ;
A6: b "\/" ((b "/\" a) "\/" ((b `) "/\" (a `))) = (b "\/" (b "/\" a)) "\/" ((b `) "/\" (a `)) by LATTICES:def_5;
A7: (Bottom B) "\/" ((b `) "/\" a) = (b `) "/\" a ;
A8: b <=> a = (b "/\" a) "\/" ((b `) "/\" (a `)) by Th50;
A9: (b `) "/\" b = Bottom B by LATTICES:20;
A11: (b `) "/\" ((a `) "/\" b) = ((b `) "/\" (a `)) "/\" b by LATTICES:def_7;
A12: b "\/" (Bottom B) = b ;
A14: (b `) "/\" ((b `) "/\" a) = ((b `) "/\" (b `)) "/\" a by LATTICES:def_7;
A15: (b <=> a) ` = (b "/\" (a `)) "\/" ((b `) "/\" a) by Th51;
A16: (b `) "/\" (b "/\" (a `)) = ((b `) "/\" b) "/\" (a `) by LATTICES:def_7;
A17: (b "\/" ((b `) "/\" (a `))) "/\" b = (b "/\" b) "\/" (((b `) "/\" (a `)) "/\" b) by LATTICES:def_11;
A18: (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, A15, A4, A16, A9, A14, A5, A7, A8, A6, A18, A17, A11, A12, LATTICES:def_5
.= b "\/" ((b "\/" (b `)) "/\" a) by LATTICES:def_11
.= b "\/" ((Top B) "/\" a) by LATTICES:21
.= b "\/" a ;
::_thesis: verum
end;
set S = LattRel [:(B /\/ <.a.)),(latt <.a.)):];
A19: field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] by Th32;
reconsider o1 = H1(B), o2 = H2(B) as BinOp of equivalence_wrt <.a.) by Th13, Th14;
A20: LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) by Def5;
set R = LattRel B;
deffunc H4( Element of B) -> Element of the carrier of B = ($1 "\/" ($1 <=> a)) <=> $1;
consider h being UnOp of the carrier of B such that
A21: for b being Element of B holds h . b = H4(b) from FUNCT_2:sch_4();
take f = <:g,h:>; :: according to WELLORD1:def_8,FILTER_1:def_9 ::_thesis: f is_isomorphism_of LattRel B, LattRel [:(B /\/ <.a.)),(latt <.a.)):]
A22: field (LattRel B) = the carrier of B by Th32;
A23: dom h = dom g by A1, FUNCT_2:def_1;
hence A24: dom f = field (LattRel B) by A1, A22, FUNCT_3:50; :: according to WELLORD1:def_7 ::_thesis: ( rng f = field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel B or ( b1 in field (LattRel B) & b2 in field (LattRel B) & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b1 in field (LattRel B) or not b2 in field (LattRel B) or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b1,b2] in LattRel B ) ) ) )
A25: for b being Element of B holds h . b is Element of (latt <.a.))
proof
let b be Element of B; ::_thesis: h . b is Element of (latt <.a.))
b "\/" (b <=> a) in Class ((equivalence_wrt <.a.)),b) by Th60;
then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:19;
then A26: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def_11;
h . b = (b "\/" (b <=> a)) <=> b by A21;
hence h . b is Element of (latt <.a.)) by A26, FILTER_0:49; ::_thesis: verum
end;
thus rng f c= field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) :: according to XBOOLE_0:def_10 ::_thesis: ( field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f & f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel B or ( b1 in field (LattRel B) & b2 in field (LattRel B) & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b1 in field (LattRel B) or not b2 in field (LattRel B) or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b1,b2] in LattRel B ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) )
assume x in rng f ; ::_thesis: x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):])
then consider y being set such that
A27: y in dom f and
A28: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of B by A1, A23, A27, FUNCT_3:50;
reconsider z2 = h . y as Element of (latt <.a.)) by A25;
g . y = EqClass ((equivalence_wrt <.a.)),y) by A1;
then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A20;
x = [z1,z2] by A27, A28, FUNCT_3:def_7;
hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A19; ::_thesis: verum
end;
A29: the carrier of (latt <.a.)) = <.a.) by FILTER_0:49;
thus field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f ::_thesis: ( f is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in LattRel B or ( b1 in field (LattRel B) & b2 in field (LattRel B) & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b1 in field (LattRel B) or not b2 in field (LattRel B) or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b1,b2] in LattRel B ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) or x in rng f )
assume x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) ; ::_thesis: x in rng f
then consider y being Element of Class (equivalence_wrt <.a.)), z being Element of <.a.) such that
A30: x = [y,z] by A19, A29, A20, DOMAIN_1:1;
consider b being Element of B such that
A31: y = Class ((equivalence_wrt <.a.)),b) by EQREL_1:36;
set ty = b "\/" (b <=> a);
(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th53;
then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;
then A32: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def_11;
b "\/" (b <=> a) in y by A31, Th60;
then y = Class ((equivalence_wrt <.a.)),(b "\/" (b <=> a))) by A31, EQREL_1:23;
then A33: (b "\/" (b <=> a)) <=> z in y by A32, EQREL_1:19;
then A34: y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A31, EQREL_1:23;
then A35: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by A31, Th60;
y = Class ((equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z)) by A31, A33, EQREL_1:23;
then A36: g . ((b "\/" (b <=> a)) <=> z) = y by A1;
((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by A31, A34, Th60;
then A37: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by A35, LATTICES:8;
h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A21;
then h . ((b "\/" (b <=> a)) <=> z) = z by A37, Th53;
then x = f . ((b "\/" (b <=> a)) <=> z) by A22, A24, A30, A36, FUNCT_3:def_7;
hence x in rng f by A22, A24, FUNCT_1:def_3; ::_thesis: verum
end;
thus f is one-to-one ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in LattRel B or ( b1 in field (LattRel B) & b2 in field (LattRel B) & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b1 in field (LattRel B) or not b2 in field (LattRel B) or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b1,b2] in LattRel B ) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A38: x in dom f and
A39: y in dom f ; ::_thesis: ( not f . x = f . y or x = y )
reconsider x9 = x, y9 = y as Element of B by A1, A23, A38, A39, FUNCT_3:50;
assume A40: f . x = f . y ; ::_thesis: x = y
A41: g . y9 = Class ((equivalence_wrt <.a.)),y9) by A1;
A42: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
A43: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A44: g . x9 = Class ((equivalence_wrt <.a.)),x9) by A1;
A45: f . y = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def_7;
A46: f . x = [(g . x9),(h . x9)] by A22, A24, FUNCT_3:def_7;
then A47: g . x = g . y by A45, A40, XTUPLE_0:1;
then A48: y9 "\/" (y9 <=> a) [= x9 "\/" (x9 <=> a) by A44, A41, Th60;
x9 "\/" (x9 <=> a) [= y9 "\/" (y9 <=> a) by A44, A41, A47, Th60;
then A49: y9 "\/" (y9 <=> a) = x9 "\/" (x9 <=> a) by A48, LATTICES:8;
h . x = h . y by A46, A45, A40, XTUPLE_0:1;
hence x = y by A43, A42, A49, Th52; ::_thesis: verum
end;
let x, y be set ; ::_thesis: ( ( not [x,y] in LattRel B or ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B ) )
A50: the carrier of (latt <.a.)) = <.a.) by FILTER_0:49;
thus ( [x,y] in LattRel B implies ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) ::_thesis: ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )
proof
assume A51: [x,y] in LattRel B ; ::_thesis: ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] )
then reconsider x9 = x, y9 = y as Element of B by A22, RELAT_1:15;
A52: x9 [= y9 by A51, Th31;
thus ( x in field (LattRel B) & y in field (LattRel B) ) by A51, RELAT_1:15; ::_thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]
A53: Top B in <.a.) by FILTER_0:11;
x9 "/\" (Top B) = x9 ;
then Top B [= x9 => y9 by A52, FILTER_0:def_7;
then x9 => y9 in <.a.) by A53, FILTER_0:9;
then A54: x9 /\/ <.a.) [= y9 /\/ <.a.) by Th16;
A55: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A56: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;
A57: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A58: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A59: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A50, A55, A59, A56, Lm4;
A60: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;
x9 "\/" a [= y9 "\/" a by A52, FILTER_0:1;
then hx [= hy by A55, A59, A58, A57, FILTER_0:51;
then A61: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A54, Th36;
A62: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;
A63: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;
A64: f . y9 = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def_7;
A65: f . x9 = [(g . x9),(h . x9)] by A22, A24, FUNCT_3:def_7;
x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;
hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] by A60, A62, A63, A65, A64, A61; ::_thesis: verum
end;
assume that
A66: x in field (LattRel B) and
A67: y in field (LattRel B) ; ::_thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )
reconsider x9 = x, y9 = y as Element of B by A66, A67, Th32;
A68: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A21;
A69: f . y9 = [(g . y9),(h . y9)] by A22, A24, FUNCT_3:def_7;
A70: y9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),y9) by Def6;
A71: Class ((equivalence_wrt <.a.)),x9) = g . x9 by A1;
A72: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A73: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A74: y9 "/\" x9 [= y9 by LATTICES:6;
A75: y9 "\/" (y9 <=> a) in Class ((equivalence_wrt <.a.)),y9) by Th60;
A76: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A21;
x9 "\/" (x9 <=> a) in Class ((equivalence_wrt <.a.)),x9) by Th60;
then reconsider hx = h . x, hy = h . y as Element of (latt <.a.)) by A50, A68, A76, A75, Lm4;
assume A77: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; ::_thesis: [x,y] in LattRel B
A78: f . x9 = [(g . x9),(h . x9)] by A22, A24, FUNCT_3:def_7;
A79: Class ((equivalence_wrt <.a.)),y9) = g . y9 by A1;
x9 /\/ <.a.) = Class ((equivalence_wrt <.a.)),x9) by Def6;
then A80: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A70, A71, A79, A78, A69, A77, Th31;
then x9 /\/ <.a.) [= y9 /\/ <.a.) by Th36;
then A81: x9 => y9 in <.a.) by Th16;
x9 => y9 = (x9 `) "\/" y9 by FILTER_0:42;
then a [= (x9 `) "\/" y9 by A81, FILTER_0:15;
then A82: x9 "/\" a [= x9 "/\" ((x9 `) "\/" y9) by LATTICES:9;
A83: (Bottom B) "\/" (x9 "/\" y9) = x9 "/\" y9 ;
hx [= hy by A80, Th36;
then x9 "\/" a [= y9 "\/" a by A68, A76, A73, A72, FILTER_0:51;
then A84: x9 "/\" (x9 "\/" a) [= x9 "/\" (y9 "\/" a) by LATTICES:9;
A85: x9 "/\" (x9 `) = Bottom B by LATTICES:20;
x9 "/\" ((x9 `) "\/" y9) = (x9 "/\" (x9 `)) "\/" (x9 "/\" y9) by LATTICES:def_11;
then x9 "/\" a [= y9 by A82, A85, A83, A74, LATTICES:7;
then A86: (x9 "/\" y9) "\/" (x9 "/\" a) [= y9 by A74, FILTER_0:6;
x9 [= x9 "\/" a by LATTICES:5;
then x9 "/\" (x9 "\/" a) = x9 by LATTICES:4;
then x9 [= (x9 "/\" y9) "\/" (x9 "/\" a) by A84, LATTICES:def_11;
then x9 [= y9 by A86, LATTICES:7;
hence [x,y] in LattRel B ; ::_thesis: verum
end;