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