let R, S be non empty doubleLoopStr ; :: thesis: for I being Ideal of R
for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let I be Ideal of R; :: thesis: for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: I is Ideal of S )
set Q = P .: I;
assume A1: P is RingIsomorphism ; :: thesis: P .: I is Ideal of S

A2: now

let p, x be Element of ; :: thesis: ( x in P .: I implies p * x in P .: I )
assume x in P .: I ; :: thesis: p * x in P .: I
then consider x' being set such that
A3: x' in the carrier of R and
A4: x' in I and
A5: x = P . x' by FUNCT_2:115;
reconsider x' = x' as Element of by A3;
A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then rng P = the carrier of S by QUOFIELD:def 22;
then consider p' being set such that
A7: p' in dom P and
A8: p = P . p' by FUNCT_1:def 5;
reconsider p' = p' as Element of by A7;
A9: p' * x' in I by A4, IDEAL_1:def 2;
P is RingHomomorphism by A6, QUOFIELD:def 22;
then P is multiplicative by QUOFIELD:def 21;
then p * x = P . (p' * x') by A5, A8, GROUP_6:def 7;
hence p * x in P .: I by A9, FUNCT_2:43; :: thesis: verum

end;

A10: now

let p, x be Element of ; :: thesis: ( x in P .: I implies x * p in P .: I )
assume x in P .: I ; :: thesis: x * p in P .: I
then consider x' being set such that
A11: x' in the carrier of R and
A12: x' in I and
A13: x = P . x' by FUNCT_2:115;
reconsider x' = x' as Element of by A11;
A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then rng P = the carrier of S by QUOFIELD:def 22;
then consider p' being set such that
A15: p' in dom P and
A16: p = P . p' by FUNCT_1:def 5;
reconsider p' = p' as Element of by A15;
A17: x' * p' in I by A12, IDEAL_1:def 3;
P is RingHomomorphism by A14, QUOFIELD:def 22;
then P is multiplicative by QUOFIELD:def 21;
then x * p = P . (x' * p') by A13, A16, GROUP_6:def 7;
hence x * p in P .: I by A17, FUNCT_2:43; :: thesis: verum

end;

now

let x, y be Element of ; :: thesis: ( x in P .: I & y in P .: I implies x + y in P .: I )
assume that
A18: x in P .: I and
A19: y in P .: I ; :: thesis: x + y in P .: I
consider x' being set such that
A20: x' in the carrier of R and
A21: x' in I and
A22: x = P . x' by A18, FUNCT_2:115;
consider y' being set such that
A23: y' in the carrier of R and
A24: y' in I and
A25: y = P . y' by A19, FUNCT_2:115;
reconsider x' = x', y' = y' as Element of by A20, A23;
A26: x' + y' in I by A21, A24, IDEAL_1:def 1;
( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then P is RingHomomorphism by QUOFIELD:def 22;
then P is additive by QUOFIELD:def 21;
then x + y = P . (x' + y') by A22, A25, GRCAT_1:def 13;
hence x + y in P .: I by A26, FUNCT_2:43; :: thesis: verum

end;

hence P .: I is Ideal of S by A2, A10, IDEAL_1:def 1, IDEAL_1:def 2, IDEAL_1:def 3; :: thesis: verum