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

P " is RingIsomorphism

let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P " is RingIsomorphism )

assume A1: P is RingIsomorphism ; :: thesis: P " is RingIsomorphism

then A2: P is RingEpimorphism ;

then A3: P is onto ;

A4: P is one-to-one by A1;

A5: ( P is additive & P is multiplicative & P is unity-preserving ) by A2;

for x, y being Element of S holds

( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )

then A15: P " is RingHomomorphism ;

A16: rng P = [#] S by A3;

then rng (P ") = [#] R by A4, TOPS_2:49;

then P " is onto ;

then A17: P " is RingEpimorphism by A15;

P " is one-to-one by A4, A16, TOPS_2:50;

hence P " is RingIsomorphism by A17; :: thesis: verum

P " is RingIsomorphism

let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P " is RingIsomorphism )

assume A1: P is RingIsomorphism ; :: thesis: P " is RingIsomorphism

then A2: P is RingEpimorphism ;

then A3: P is onto ;

A4: P is one-to-one by A1;

A5: ( P is additive & P is multiplicative & P is unity-preserving ) by A2;

for x, y being Element of S holds

( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )

proof

then
( P " is additive & P " is multiplicative & P " is unity-preserving )
by GROUP_1:def 13;
A6:
P is onto
by A3;

A7: (P ") . (1_ S) = (P ") . (P . (1_ R)) by A5, GROUP_1:def 13

.= (P ") . (P . (1_ R)) by A4, A6, TOPS_2:def 4

.= 1_ R by A4, FUNCT_2:26 ;

let x, y be Element of S; :: thesis: ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )

consider x9 being object such that

A8: x9 in the carrier of R and

A9: P . x9 = x by A3, FUNCT_2:11;

reconsider x9 = x9 as Element of R by A8;

A10: x9 = (P ") . (P . x9) by A4, FUNCT_2:26

.= (P ") . x by A4, A9, A6, TOPS_2:def 4 ;

consider y9 being object such that

A11: y9 in the carrier of R and

A12: P . y9 = y by A3, FUNCT_2:11;

reconsider y9 = y9 as Element of R by A11;

A13: y9 = (P ") . (P . y9) by A4, FUNCT_2:26

.= (P ") . y by A6, A4, A12, TOPS_2:def 4 ;

A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12

.= (P ") . (P . (x9 * y9)) by A4, A6, TOPS_2:def 4

.= ((P ") . x) * ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;

(P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12

.= (P ") . (P . (x9 + y9)) by A4, A6, TOPS_2:def 4

.= ((P ") . x) + ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;

hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by A14, A7; :: thesis: verum

end;A7: (P ") . (1_ S) = (P ") . (P . (1_ R)) by A5, GROUP_1:def 13

.= (P ") . (P . (1_ R)) by A4, A6, TOPS_2:def 4

.= 1_ R by A4, FUNCT_2:26 ;

let x, y be Element of S; :: thesis: ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )

consider x9 being object such that

A8: x9 in the carrier of R and

A9: P . x9 = x by A3, FUNCT_2:11;

reconsider x9 = x9 as Element of R by A8;

A10: x9 = (P ") . (P . x9) by A4, FUNCT_2:26

.= (P ") . x by A4, A9, A6, TOPS_2:def 4 ;

consider y9 being object such that

A11: y9 in the carrier of R and

A12: P . y9 = y by A3, FUNCT_2:11;

reconsider y9 = y9 as Element of R by A11;

A13: y9 = (P ") . (P . y9) by A4, FUNCT_2:26

.= (P ") . y by A6, A4, A12, TOPS_2:def 4 ;

A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12

.= (P ") . (P . (x9 * y9)) by A4, A6, TOPS_2:def 4

.= ((P ") . x) * ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;

(P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12

.= (P ") . (P . (x9 + y9)) by A4, A6, TOPS_2:def 4

.= ((P ") . x) + ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;

hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by A14, A7; :: thesis: verum

then A15: P " is RingHomomorphism ;

A16: rng P = [#] S by A3;

then rng (P ") = [#] R by A4, TOPS_2:49;

then P " is onto ;

then A17: P " is RingEpimorphism by A15;

P " is one-to-one by A4, A16, TOPS_2:50;

hence P " is RingIsomorphism by A17; :: thesis: verum