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 ) )

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

let p2 be Element of L2; :: according to LATTICES:def 12 :: thesis: for b_{1}, b_{2} being Element of the carrier of L2 holds

( not p2 [= b_{2} or p2 "\/" (b_{1} "/\" b_{2}) = (p2 "\/" b_{1}) "/\" b_{2} )

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

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 A9:
for a, b, c being Element of [:L1,L2:] st a [= c holds
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;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

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 p1 = the Element of L1;
set p2 = the Element of L2;

let p1 be Element of L1; :: according to LATTICES:def 12 :: thesis: for b_{1}, b_{2} being Element of the carrier of L1 holds

( not p1 [= b_{2} or p1 "\/" (b_{1} "/\" b_{2}) = (p1 "\/" b_{1}) "/\" b_{2} )

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;let p1 be Element of L1; :: according to LATTICES:def 12 :: thesis: for b

( not p1 [= b

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

let p2 be Element of L2; :: according to LATTICES:def 12 :: thesis: for b

( not p2 [= b

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