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