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

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 :: thesis: for p, x being Element of S st x in P .: I holds

p * x in P .: I

p * x in P .: I

let p, x be Element of S; :: thesis: ( x in P .: I implies p * x in P .: I )

assume x in P .: I ; :: thesis: p * x in P .: I

then consider x9 being object such that

A3: x9 in the carrier of R and

A4: x9 in I and

A5: x = P . x9 by FUNCT_2:64;

reconsider x9 = x9 as Element of R by A3;

A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is onto ;

then consider p9 being object such that

A7: p9 in dom P and

A8: p = P . p9 by FUNCT_1:def 3;

reconsider p9 = p9 as Element of R by A7;

A9: p9 * x9 in I by A4, IDEAL_1:def 2;

P is RingHomomorphism by A6;

then P is multiplicative ;

then p * x = P . (p9 * x9) by A5, A8;

hence p * x in P .: I by A9, FUNCT_2:35; :: thesis: verum

end;assume x in P .: I ; :: thesis: p * x in P .: I

then consider x9 being object such that

A3: x9 in the carrier of R and

A4: x9 in I and

A5: x = P . x9 by FUNCT_2:64;

reconsider x9 = x9 as Element of R by A3;

A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is onto ;

then consider p9 being object such that

A7: p9 in dom P and

A8: p = P . p9 by FUNCT_1:def 3;

reconsider p9 = p9 as Element of R by A7;

A9: p9 * x9 in I by A4, IDEAL_1:def 2;

P is RingHomomorphism by A6;

then P is multiplicative ;

then p * x = P . (p9 * x9) by A5, A8;

hence p * x in P .: I by A9, FUNCT_2:35; :: thesis: verum

A10: now :: thesis: for p, x being Element of S st x in P .: I holds

x * p in P .: I

x * p in P .: I

let p, x be Element of S; :: thesis: ( x in P .: I implies x * p in P .: I )

assume x in P .: I ; :: thesis: x * p in P .: I

then consider x9 being object such that

A11: x9 in the carrier of R and

A12: x9 in I and

A13: x = P . x9 by FUNCT_2:64;

reconsider x9 = x9 as Element of R by A11;

A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is onto ;

then consider p9 being object such that

A15: p9 in dom P and

A16: p = P . p9 by FUNCT_1:def 3;

reconsider p9 = p9 as Element of R by A15;

A17: x9 * p9 in I by A12, IDEAL_1:def 3;

P is RingHomomorphism by A14;

then P is multiplicative ;

then x * p = P . (x9 * p9) by A13, A16;

hence x * p in P .: I by A17, FUNCT_2:35; :: thesis: verum

end;assume x in P .: I ; :: thesis: x * p in P .: I

then consider x9 being object such that

A11: x9 in the carrier of R and

A12: x9 in I and

A13: x = P . x9 by FUNCT_2:64;

reconsider x9 = x9 as Element of R by A11;

A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is onto ;

then consider p9 being object such that

A15: p9 in dom P and

A16: p = P . p9 by FUNCT_1:def 3;

reconsider p9 = p9 as Element of R by A15;

A17: x9 * p9 in I by A12, IDEAL_1:def 3;

P is RingHomomorphism by A14;

then P is multiplicative ;

then x * p = P . (x9 * p9) by A13, A16;

hence x * p in P .: I by A17, FUNCT_2:35; :: thesis: verum

now :: thesis: for x, y being Element of S st x in P .: I & y in P .: I holds

x + y in P .: I

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

let x, y be Element of S; :: 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 x9 being object such that

A20: x9 in the carrier of R and

A21: x9 in I and

A22: x = P . x9 by A18, FUNCT_2:64;

consider y9 being object such that

A23: y9 in the carrier of R and

A24: y9 in I and

A25: y = P . y9 by A19, FUNCT_2:64;

reconsider x9 = x9, y9 = y9 as Element of R by A20, A23;

A26: x9 + y9 in I by A21, A24, IDEAL_1:def 1;

( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is additive ;

then x + y = P . (x9 + y9) by A22, A25;

hence x + y in P .: I by A26, FUNCT_2:35; :: thesis: verum

end;assume that

A18: x in P .: I and

A19: y in P .: I ; :: thesis: x + y in P .: I

consider x9 being object such that

A20: x9 in the carrier of R and

A21: x9 in I and

A22: x = P . x9 by A18, FUNCT_2:64;

consider y9 being object such that

A23: y9 in the carrier of R and

A24: y9 in I and

A25: y = P . y9 by A19, FUNCT_2:64;

reconsider x9 = x9, y9 = y9 as Element of R by A20, A23;

A26: x9 + y9 in I by A21, A24, IDEAL_1:def 1;

( P is RingMonomorphism & P is RingEpimorphism ) by A1;

then P is additive ;

then x + y = P . (x9 + y9) by A22, A25;

hence x + y in P .: I by A26, FUNCT_2:35; :: thesis: verum