let R, S be non empty doubleLoopStr ; for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism
let P be Function of R,S; ( P is RingIsomorphism implies P " is RingIsomorphism )
assume A1:
P is RingIsomorphism
; 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
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;
( (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;
verum
end;
then
( P " is additive & P " is multiplicative & P " is unity-preserving )
by GROUP_1:def 13;
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; verum