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 p1 being
Element of
L1,
p2 being
Element of
L2 such that A4:
a = [p1,p2]
by DOMAIN_1:9;
consider q1 being
Element of
L1,
q2 being
Element of
L2 such that A5:
b = [q1,q2]
by DOMAIN_1:9;
consider r1 being
Element of
L1,
r2 being
Element of
L2 such that A6:
c = [r1,r2]
by DOMAIN_1:9;
A7:
(
p1 [= r1 &
p2 [= r2 )
by A3, A4, A6, Th37;
thus a "\/" (b "/\" c) =
a "\/" [(q1 "/\" r1),(q2 "/\" r2)]
by A5, A6, Th22
.=
[(p1 "\/" (q1 "/\" r1)),(p2 "\/" (q2 "/\" r2))]
by A4, Th22
.=
[((p1 "\/" q1) "/\" r1),(p2 "\/" (q2 "/\" r2))]
by A1, A7
.=
[((p1 "\/" q1) "/\" r1),((p2 "\/" q2) "/\" r2)]
by A2, A7
.=
[(p1 "\/" q1),(p2 "\/" q2)] "/\" c
by A6, Th22
.=
(a "\/" b) "/\" c
by A4, A5, Th22
;
:: thesis: verum
end;
assume A8:
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
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 A9:
p1 [= r1
;
:: thesis: p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1
consider p2,
q2 being
Element of
L2;
[p1,p2] [= [r1,p2]
by A9, Th37;
then
(
[p1,p2] "\/" ([q1,q2] "/\" [r1,p2]) = ([p1,p2] "\/" [q1,q2]) "/\" [r1,p2] &
[q1,q2] "/\" [r1,p2] = [(q1 "/\" r1),(q2 "/\" p2)] &
[p1,p2] "\/" [q1,q2] = [(p1 "\/" q1),(p2 "\/" q2)] &
[p1,p2] "\/" [(q1 "/\" r1),(q2 "/\" p2)] = [(p1 "\/" (q1 "/\" r1)),(p2 "\/" (q2 "/\" p2))] &
[(p1 "\/" q1),(p2 "\/" q2)] "/\" [r1,p2] = [((p1 "\/" q1) "/\" r1),((p2 "\/" q2) "/\" p2)] )
by A8, Th22;
hence
p1 "\/" (q1 "/\" r1) = (p1 "\/" q1) "/\" r1
by ZFMISC_1:33;
:: thesis: verum
end;
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 A10:
p2 [= r2
; :: thesis: p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2
consider p1, q1 being Element of L1;
[p1,p2] [= [p1,r2]
by A10, Th37;
then
( [p1,p2] "\/" ([q1,q2] "/\" [p1,r2]) = ([p1,p2] "\/" [q1,q2]) "/\" [p1,r2] & [q1,q2] "/\" [p1,r2] = [(q1 "/\" p1),(q2 "/\" r2)] & [p1,p2] "\/" [q1,q2] = [(p1 "\/" q1),(p2 "\/" q2)] & [p1,p2] "\/" [(q1 "/\" p1),(q2 "/\" r2)] = [(p1 "\/" (q1 "/\" p1)),(p2 "\/" (q2 "/\" r2))] & [(p1 "\/" q1),(p2 "\/" q2)] "/\" [p1,r2] = [((p1 "\/" q1) "/\" p1),((p2 "\/" q2) "/\" r2)] )
by A8, Th22;
hence
p2 "\/" (q2 "/\" r2) = (p2 "\/" q2) "/\" r2
by ZFMISC_1:33; :: thesis: verum