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

reconsider f = f as Homomorphism of IL,CL ;

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

then reconsider CL = CL as implicative Lattice ;
let p, q be Element of CL; :: according to FILTER_0:def 6 :: thesis: ex b_{1} being Element of the carrier of CL st

( p "/\" b_{1} [= q & ( for b_{2} being Element of the carrier of CL holds

( not p "/\" b_{2} [= q or b_{2} [= b_{1} ) ) )

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_{1} being Element of the carrier of CL holds

( not p "/\" b_{1} [= q or b_{1} [= r ) ) )

thus p "/\" r [= q by A2, A3, Th26; :: thesis: for b_{1} being Element of the carrier of CL holds

( not p "/\" b_{1} [= q or b_{1} [= r )

end;( p "/\" b

( not p "/\" 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

( not p "/\" b

thus p "/\" r [= q by A2, A3, Th26; :: thesis: for b

( not p "/\" b

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;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

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)

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

hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def 7; :: thesis: verum

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

r1 [= f . (i => j)

(f . i) "/\" (f . (i => j)) [= f . j
by Th26;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;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

hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def 7; :: thesis: verum