let R, S be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for F being non empty Subset of R

for P being Function of R,S st P is RingIsomorphism holds

P .: (F -Ideal) = (P .: F) -Ideal

let F be non empty Subset of R; :: thesis: for P being Function of R,S st P is RingIsomorphism holds

P .: (F -Ideal) = (P .: F) -Ideal

let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: (F -Ideal) = (P .: F) -Ideal )

assume A1: P is RingIsomorphism ; :: thesis: P .: (F -Ideal) = (P .: F) -Ideal

hence P .: (F -Ideal) = (P .: F) -Ideal by A10, XBOOLE_0:def 10; :: thesis: verum

for P being Function of R,S st P is RingIsomorphism holds

P .: (F -Ideal) = (P .: F) -Ideal

let F be non empty Subset of R; :: thesis: for P being Function of R,S st P is RingIsomorphism holds

P .: (F -Ideal) = (P .: F) -Ideal

let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: (F -Ideal) = (P .: F) -Ideal )

assume A1: P is RingIsomorphism ; :: thesis: P .: (F -Ideal) = (P .: F) -Ideal

now :: thesis: for x being object st x in (P .: F) -Ideal holds

x in P .: (F -Ideal)

then A10:
(P .: F) -Ideal c= P .: (F -Ideal)
;x in P .: (F -Ideal)

let x be object ; :: thesis: ( x in (P .: F) -Ideal implies x in P .: (F -Ideal) )

A2: dom P = the carrier of R by FUNCT_2:def 1;

assume A3: x in (P .: F) -Ideal ; :: thesis: x in P .: (F -Ideal)

then consider lc being LinearCombination of P .: F such that

A4: x = Sum lc by IDEAL_1:60;

consider E being FinSequence of [: the carrier of S, the carrier of S, the carrier of S:] such that

A5: E represents lc by IDEAL_1:35;

P is RingMonomorphism by A1;

then A6: P is one-to-one ;

A7: P is onto by A1;

then A8: P " = P " by A6, TOPS_2:def 4;

(P ") .: (P .: F) = P " (P .: F) by A6, FUNCT_1:85;

then consider lc9 being LinearCombination of F such that

A9: ( len lc = len lc9 & ( for i being set st i in dom lc9 holds

lc9 . i = (((P ") . ((E /. i) `1_3)) * ((P ") . ((E /. i) `2_3))) * ((P ") . ((E /. i) `3_3)) ) ) by A6, A8, A5, FUNCT_1:82, IDEAL_1:36;

P " is RingIsomorphism by A1, Th25;

then P " is RingMonomorphism ;

then P " is RingHomomorphism ;

then (P ") . x = Sum lc9 by A4, A5, A9, Th24;

then (P ") . x in F -Ideal by IDEAL_1:60;

then P . ((P ") . x) in P .: (F -Ideal) by A2, FUNCT_1:def 6;

hence x in P .: (F -Ideal) by A3, A6, A7, A8, FUNCT_1:35; :: thesis: verum

end;A2: dom P = the carrier of R by FUNCT_2:def 1;

assume A3: x in (P .: F) -Ideal ; :: thesis: x in P .: (F -Ideal)

then consider lc being LinearCombination of P .: F such that

A4: x = Sum lc by IDEAL_1:60;

consider E being FinSequence of [: the carrier of S, the carrier of S, the carrier of S:] such that

A5: E represents lc by IDEAL_1:35;

P is RingMonomorphism by A1;

then A6: P is one-to-one ;

A7: P is onto by A1;

then A8: P " = P " by A6, TOPS_2:def 4;

(P ") .: (P .: F) = P " (P .: F) by A6, FUNCT_1:85;

then consider lc9 being LinearCombination of F such that

A9: ( len lc = len lc9 & ( for i being set st i in dom lc9 holds

lc9 . i = (((P ") . ((E /. i) `1_3)) * ((P ") . ((E /. i) `2_3))) * ((P ") . ((E /. i) `3_3)) ) ) by A6, A8, A5, FUNCT_1:82, IDEAL_1:36;

P " is RingIsomorphism by A1, Th25;

then P " is RingMonomorphism ;

then P " is RingHomomorphism ;

then (P ") . x = Sum lc9 by A4, A5, A9, Th24;

then (P ") . x in F -Ideal by IDEAL_1:60;

then P . ((P ") . x) in P .: (F -Ideal) by A2, FUNCT_1:def 6;

hence x in P .: (F -Ideal) by A3, A6, A7, A8, FUNCT_1:35; :: thesis: verum

now :: thesis: for x being object st x in P .: (F -Ideal) holds

x in (P .: F) -Ideal

then
P .: (F -Ideal) c= (P .: F) -Ideal
;x in (P .: F) -Ideal

let x be object ; :: thesis: ( x in P .: (F -Ideal) implies x in (P .: F) -Ideal )

assume x in P .: (F -Ideal) ; :: thesis: x in (P .: F) -Ideal

then consider x9 being object such that

x9 in the carrier of R and

A11: x9 in F -Ideal and

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

consider lc9 being LinearCombination of F such that

A13: x9 = Sum lc9 by A11, IDEAL_1:60;

consider E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] such that

A14: E represents lc9 by IDEAL_1:35;

consider lc being LinearCombination of P .: F such that

A15: ( len lc9 = len lc & ( for i being set st i in dom lc holds

lc . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) ) by A14, IDEAL_1:36;

P is RingMonomorphism by A1;

then P is RingHomomorphism ;

then x = Sum lc by A12, A13, A14, A15, Th24;

hence x in (P .: F) -Ideal by IDEAL_1:60; :: thesis: verum

end;assume x in P .: (F -Ideal) ; :: thesis: x in (P .: F) -Ideal

then consider x9 being object such that

x9 in the carrier of R and

A11: x9 in F -Ideal and

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

consider lc9 being LinearCombination of F such that

A13: x9 = Sum lc9 by A11, IDEAL_1:60;

consider E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] such that

A14: E represents lc9 by IDEAL_1:35;

consider lc being LinearCombination of P .: F such that

A15: ( len lc9 = len lc & ( for i being set st i in dom lc holds

lc . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) ) by A14, IDEAL_1:36;

P is RingMonomorphism by A1;

then P is RingHomomorphism ;

then x = Sum lc by A12, A13, A14, A15, Th24;

hence x in (P .: F) -Ideal by IDEAL_1:60; :: thesis: verum

hence P .: (F -Ideal) = (P .: F) -Ideal by A10, XBOOLE_0:def 10; :: thesis: verum