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 ;

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 `)

hence
f preserves_complement
; :: thesis: verumlet 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;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