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 7 :: 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 7 :: thesis: [:L1,L2:] is implicative
let a,
b be
Element of
[:L1,L2:];
:: according to FILTER_0:def 7 :: 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:9;
consider q1 being
Element of
L1,
q2 being
Element of
L2 such that A4:
b = [q1,q2]
by DOMAIN_1:9;
consider r1 being
Element of
L1 such that A5:
(
p1 "/\" r1 [= q1 & ( for
s1 being
Element of
L1 st
p1 "/\" s1 [= q1 holds
s1 [= r1 ) )
by A1;
consider r2 being
Element of
L2 such that A6:
(
p2 "/\" r2 [= q2 & ( for
s2 being
Element of
L2 st
p2 "/\" s2 [= q2 holds
s2 [= r2 ) )
by A2;
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, Th22;
hence
a "/\" [r1,r2] [= b
by A4, A5, A6, Th37;
:: 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 A7:
d = [s1,s2]
by DOMAIN_1:9;
assume
a "/\" d [= b
;
:: thesis: d [= [r1,r2]
then
[(p1 "/\" s1),(p2 "/\" s2)] [= b
by A3, A7, Th22;
then
(
p1 "/\" s1 [= q1 &
p2 "/\" s2 [= q2 )
by A4, Th37;
then
(
s1 [= r1 &
s2 [= r2 )
by A5, A6;
hence
d [= [r1,r2]
by A7, Th37;
:: thesis: verum
end;
assume A8:
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 7 :: 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 7 :: thesis: L2 is implicative proof
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 p2,
q2 being
Element of
L2;
consider c being
Element of
[:L1,L2:] such that A9:
(
[p1,p2] "/\" c [= [q1,q2] & ( for
d being
Element of
[:L1,L2:] st
[p1,p2] "/\" d [= [q1,q2] holds
d [= c ) )
by A8;
consider r1 being
Element of
L1,
r2 being
Element of
L2 such that A10:
c = [r1,r2]
by DOMAIN_1:9;
take
r1
;
:: thesis: ( p1 "/\" r1 [= q1 & ( for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1 ) )
A11:
[p1,p2] "/\" c = [(p1 "/\" r1),(p2 "/\" r2)]
by A10, Th22;
then A12:
(
p1 "/\" r1 [= q1 &
p2 "/\" r2 [= q2 )
by A9, Th37;
thus
p1 "/\" r1 [= q1
by A9, A11, Th37;
:: 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
p1 "/\" s1 [= q1
;
:: thesis: s1 [= r1
then
[(p1 "/\" s1),(p2 "/\" r2)] [= [q1,q2]
by A12, Th37;
then
[p1,p2] "/\" [s1,r2] [= [q1,q2]
by Th22;
then
[s1,r2] [= c
by A9;
hence
s1 [= r1
by A10, Th37;
:: thesis: verum
end;
let p2 be Element of L2; :: according to FILTER_0:def 7 :: 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 p1, q1 being Element of L1;
consider c being Element of [:L1,L2:] such that
A13:
( [p1,p2] "/\" c [= [q1,q2] & ( for d being Element of [:L1,L2:] st [p1,p2] "/\" d [= [q1,q2] holds
d [= c ) )
by A8;
consider r1 being Element of L1, r2 being Element of L2 such that
A14:
c = [r1,r2]
by DOMAIN_1:9;
take
r2
; :: thesis: ( p2 "/\" r2 [= q2 & ( for b1 being Element of the carrier of L2 holds
( not p2 "/\" b1 [= q2 or b1 [= r2 ) ) )
A15:
[p1,p2] "/\" c = [(p1 "/\" r1),(p2 "/\" r2)]
by A14, Th22;
then A16:
( p1 "/\" r1 [= q1 & p2 "/\" r2 [= q2 )
by A13, Th37;
thus
p2 "/\" r2 [= q2
by A13, A15, Th37; :: 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
p2 "/\" s2 [= q2
; :: thesis: s2 [= r2
then
[(p1 "/\" r1),(p2 "/\" s2)] [= [q1,q2]
by A16, Th37;
then
[p1,p2] "/\" [r1,s2] [= [q1,q2]
by Th22;
then
[r1,s2] [= c
by A13;
hence
s2 [= r2
by A14, Th37; :: thesis: verum