let L1, L2 be lower-bounded LATTICE; ( L1,L2 are_isomorphic & L1 is modular implies L2 is modular )
assume that
A1:
L1,L2 are_isomorphic
and
A2:
L1 is modular
; L2 is modular
let a, b, c be Element of L2; YELLOW11:def 3 ( not a <= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
consider f being Function of L1,L2 such that
A3:
f is isomorphic
by A1, WAYBEL_1:def 8;
set C = (f ") . c;
set A = (f ") . a;
set B = (f ") . b;
A4:
( f is V17() & rng f = the carrier of L2 )
by A3, WAYBEL_0:66;
then A5:
b = f . ((f ") . b)
by FUNCT_1:35;
A6:
(f ") . c in dom f
by A4, FUNCT_1:32;
A7:
( (f ") . a in dom f & (f ") . b in dom f )
by A4, FUNCT_1:32;
A8:
( a = f . ((f ") . a) & c = f . ((f ") . c) )
by A4, FUNCT_1:35;
reconsider A = (f ") . a, B = (f ") . b, C = (f ") . c as Element of L1 by A7, A6;
assume
a <= c
; a "\/" (b "/\" c) = (a "\/" b) "/\" c
then
A <= C
by A3, A8, WAYBEL_0:66;
then A9:
A "\/" (B "/\" C) = (A "\/" B) "/\" C
by A2;
( f is infs-preserving & f is sups-preserving )
by A3, WAYBEL13:20;
then A10:
( f is meet-preserving & f is join-preserving )
;
hence a "\/" (b "/\" c) =
(f . A) "\/" (f . (B "/\" C))
by A5, A8, WAYBEL_6:1
.=
f . ((A "\/" B) "/\" C)
by A10, A9, WAYBEL_6:2
.=
(f . (A "\/" B)) "/\" (f . C)
by A10, WAYBEL_6:1
.=
(a "\/" b) "/\" c
by A10, A5, A8, WAYBEL_6:2
;
verum