let L1, L2 be Lattice; ( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )
thus
( L1 is implicative & L2 is implicative implies [:L1,L2:] is implicative )
( [: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 ) )
;
FILTER_0:def 6 ( 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 ) )
;
FILTER_0:def 6 [:L1,L2:] is implicative
let a,
b be
Element of
[:L1,L2:];
FILTER_0:def 6 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]
;
( 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;
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:];
( 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
;
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;
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 ) )
; FILTER_0:def 6 ( 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 ) )
FILTER_0:def 6 L2 is implicative proof
set p2 = the
Element of
L2;
let p1,
q1 be
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 ) )
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
;
( 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;
for s1 being Element of L1 st p1 "/\" s1 [= q1 holds
s1 [= r1
let s1 be
Element of
L1;
( p1 "/\" s1 [= q1 implies s1 [= r1 )
assume A17:
p1 "/\" s1 [= q1
;
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;
verum
end;
set p1 = the Element of L1;
let p2 be Element of L2; FILTER_0:def 6 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; 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
; ( 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; for b1 being Element of the carrier of L2 holds
( not p2 "/\" b1 [= q2 or b1 [= r2 )
let s2 be Element of L2; ( not p2 "/\" s2 [= q2 or s2 [= r2 )
assume A22:
p2 "/\" s2 [= q2
; 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; verum