let CL be C_Lattice; :: thesis: for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )
let IL be implicative Lattice; :: thesis: for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )
let f be Homomorphism of IL,CL; :: thesis: ( f is bijective implies ( CL is implicative & f preserves_implication ) )
assume A1: f is bijective ; :: thesis: ( CL is implicative & f preserves_implication )
thus CL is implicative :: thesis: f preserves_implication

proof

let p, q be Element of CL; :: according to FILTER_0:def 6 :: thesis: ex b₁ being Element of the carrier of CL st
( p "/\" b₁ [= q & ( for b₂ being Element of the carrier of CL holds
( not p "/\" b₂ [= q or b₂ [= b₁ ) ) )
consider i being Element of IL such that
A2: f . i = p by A1, Th6;
consider j being Element of IL such that
A3: f . j = q by A1, Th6;
take r = f . (i => j); :: thesis: ( p "/\" r [= q & ( for b₁ being Element of the carrier of CL holds
( not p "/\" b₁ [= q or b₁ [= r ) ) )
thus p "/\" r [= q by A2, A3, Th26; :: thesis: for b₁ being Element of the carrier of CL holds
( not p "/\" b₁ [= q or b₁ [= r )

hereby :: thesis: verum

let r1 be Element of CL; :: thesis: ( p "/\" r1 [= q implies r1 [= r )
assume A4: p "/\" r1 [= q ; :: thesis: r1 [= r
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= r by A1, A2, A3, A4, Th27; :: thesis: verum

end;

end;

then reconsider CL = CL as implicative Lattice ;
reconsider f = f as Homomorphism of IL,CL ;

now :: thesis: for i, j being Element of IL holds (f . i) => (f . j) = f . (i => j)

let i, j be Element of IL; :: thesis: (f . i) => (f . j) = f . (i => j)

A5: now :: thesis: for r1 being Element of CL st (f . i) "/\" r1 [= f . j holds
r1 [= f . (i => j)

let r1 be Element of CL; :: thesis: ( (f . i) "/\" r1 [= f . j implies r1 [= f . (i => j) )
assume A6: (f . i) "/\" r1 [= f . j ; :: thesis: r1 [= f . (i => j)
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= f . (i => j) by A1, A6, Th27; :: thesis: verum

end;

(f . i) "/\" (f . (i => j)) [= f . j by Th26;
hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def 7; :: thesis: verum

end;

hence f preserves_implication ; :: thesis: verum