let CL be C_Lattice; :: thesis: for BL being Boolean Lattice
for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean & f preserves_complement )
let BL be Boolean Lattice; :: thesis: for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean & f preserves_complement )
let f be Homomorphism of BL,CL; :: thesis: ( f is onto implies ( CL is Boolean & f preserves_complement ) )
assume A1: f is onto ; :: thesis: ( CL is Boolean & f preserves_complement )
then A2: f preserves_top by Th18;
thus ( CL is bounded & CL is complemented ) ; :: according to LATTICES:def 20 :: thesis: ( CL is distributive & f preserves_complement )
thus CL is distributive by A1, Th11; :: thesis: f preserves_complement
then reconsider CL = CL as Boolean Lattice ;
A3: f preserves_bottom by A1, Th12;
reconsider f = f as Homomorphism of BL,CL ;
now :: thesis: for a1 being Element of BL holds (f . a1) ` = f . (a1 `)
let a1 be Element of BL; :: thesis: (f . a1) ` = f . (a1 `)
A4: (f . (a1 `)) "/\" (f . a1) = f . ((a1 `) "/\" a1) by D2
.= f . (Bottom BL) by LATTICES:20
.= Bottom CL by A3 ;
A5: ( (f . (a1 `)) "\/" (f . a1) = (f . a1) "\/" (f . (a1 `)) & (f . (a1 `)) "/\" (f . a1) = (f . a1) "/\" (f . (a1 `)) ) ;
(f . (a1 `)) "\/" (f . a1) = f . ((a1 `) "\/" a1) by D1
.= f . (Top BL) by LATTICES:21
.= Top CL by A2 ;
then f . (a1 `) is_a_complement_of f . a1 by A4, A5;
hence (f . a1) ` = f . (a1 `) by LATTICES:def 21; :: thesis: verum
end;
hence f preserves_complement ; :: thesis: verum