:: 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;