let A, B be non degenerated commutative Ring; :: thesis: for h being Function of A,B
for M0 being prime Ideal of B st h is RingHomomorphism holds
h " M0 is prime Ideal of A
let h be Function of A,B; :: thesis: for M0 being prime Ideal of B st h is RingHomomorphism holds
h " M0 is prime Ideal of A
let M0 be prime Ideal of B; :: thesis: ( h is RingHomomorphism implies h " M0 is prime Ideal of A )
assume A1: h is RingHomomorphism ; :: thesis: h " M0 is prime Ideal of A
A2: for x, y being Element of A holds
( not x * y in h " M0 or x in h " M0 or y in h " M0 )

proof

let x, y be Element of A; :: thesis: ( not x * y in h " M0 or x in h " M0 or y in h " M0 )
assume x * y in h " M0 ; :: thesis: ( x in h " M0 or y in h " M0 )
then ( x * y in dom h & h . (x * y) in M0 ) by FUNCT_1:def 7;
then A4: (h . x) * (h . y) in M0 by A1, GROUP_6:def 6;
A5: dom h = the carrier of A by FUNCT_2:def 1;
( x in h " M0 or y in h " M0 )

proof

per cases ( h . x in M0 or h . y in M0 ) by A4, RING_1:def 1;

suppose h . x in M0 ; :: thesis: ( x in h " M0 or y in h " M0 )

hence ( x in h " M0 or y in h " M0 ) by A5, FUNCT_1:def 7; :: thesis: verum

end;

suppose h . y in M0 ; :: thesis: ( x in h " M0 or y in h " M0 )

hence ( x in h " M0 or y in h " M0 ) by A5, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence ( x in h " M0 or y in h " M0 ) ; :: thesis: verum

end;

h " M0 <> the carrier of A

proof

assume A9: h " M0 = the carrier of A ; :: thesis: contradiction
A10: h is unity-preserving by A1;
1. B in M0 by A9, FUNCT_1:def 7, A10;
hence contradiction by IDEAL_1:19; :: thesis: verum

end;

then ( h " M0 is proper & h " M0 is quasi-prime ) by A2;
hence h " M0 is prime Ideal of A by A1, Th50; :: thesis: verum