let L2 be Lattice; :: thesis: 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; :: thesis: for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let f be Homomorphism of DL,L2; :: thesis: ( f is onto implies L2 is distributive )
assume A1:
f is onto
; :: thesis: L2 is distributive
thus
L2 is distributive
:: thesis: verumproof
let a,
b,
c be
Element of
L2;
:: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
consider a' being
Element of
DL such that A2:
f . a' = a
by A1, Th9;
consider b' being
Element of
DL such that A3:
f . b' = b
by A1, Th9;
consider c' being
Element of
DL such that A4:
f . c' = c
by A1, Th9;
thus a "/\" (b "\/" c) =
a "/\" (f . (b' "\/" c'))
by A3, A4, Def1
.=
f . (a' "/\" (b' "\/" c'))
by A2, Def1
.=
f . ((a' "/\" b') "\/" (a' "/\" c'))
by LATTICES:def 11
.=
(f . (a' "/\" b')) "\/" (f . (a' "/\" c'))
by Def1
.=
(a "/\" b) "\/" (f . (a' "/\" c'))
by A2, A3, Def1
.=
(a "/\" b) "\/" (a "/\" c)
by A2, A4, Def1
;
:: thesis: verum
end;