let L2 be Lattice; for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let DL be distributive Lattice; for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let f be Homomorphism of DL,L2; ( f is onto implies L2 is distributive )
assume A1:
f is onto
; L2 is distributive
thus
L2 is distributive
verumproof
let a,
b,
c be
Element of
L2;
LATTICES:def 11 a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
consider a9 being
Element of
DL such that A2:
f . a9 = a
by A1, Th6;
consider c9 being
Element of
DL such that A3:
f . c9 = c
by A1, Th6;
consider b9 being
Element of
DL such that A4:
f . b9 = b
by A1, Th6;
thus a "/\" (b "\/" c) =
a "/\" (f . (b9 "\/" c9))
by A4, A3, D1
.=
f . (a9 "/\" (b9 "\/" c9))
by A2, D2
.=
f . ((a9 "/\" b9) "\/" (a9 "/\" c9))
by LATTICES:def 11
.=
(f . (a9 "/\" b9)) "\/" (f . (a9 "/\" c9))
by D1
.=
(a "/\" b) "\/" (f . (a9 "/\" c9))
by A2, A4, D2
.=
(a "/\" b) "\/" (a "/\" c)
by A2, A3, D2
;
verum
end;