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
by QUOFIELD:def 24;
then A3:
rng P = the carrier of S
by QUOFIELD:def 22;
P is RingMonomorphism
by A1, QUOFIELD:def 24;
then A4:
P is one-to-one
by QUOFIELD:def 23;
P is RingHomomorphism
by A2, QUOFIELD:def 22;
then A5:
( P is additive & P is multiplicative & P is unity-preserving )
by QUOFIELD:def 21;
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 " ) . (1_ S) =
(P " ) . (P . (1_ R))
by A5, GROUP_1:def 17
.=
(P " ) . (P . (1_ R))
by A4, A3, TOPS_2:def 4
.=
1_ R
by A4, FUNCT_2:32
;
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
set such that A7:
x9 in the
carrier of
R
and A8:
P . x9 = x
by A3, FUNCT_2:17;
reconsider x9 =
x9 as
Element of
R by A7;
A9:
x9 =
(P " ) . (P . x9)
by A4, FUNCT_2:32
.=
(P " ) . x
by A4, A3, A8, TOPS_2:def 4
;
consider y9 being
set such that A10:
y9 in the
carrier of
R
and A11:
P . y9 = y
by A3, FUNCT_2:17;
reconsider y9 =
y9 as
Element of
R by A10;
A12:
y9 =
(P " ) . (P . y9)
by A4, FUNCT_2:32
.=
(P " ) . y
by A4, A3, A11, TOPS_2:def 4
;
A13:
(P " ) . (x * y) =
(P " ) . (P . (x9 * y9))
by A5, A8, A11, GROUP_6:def 7
.=
(P " ) . (P . (x9 * y9))
by A4, A3, TOPS_2:def 4
.=
((P " ) . x) * ((P " ) . y)
by A4, A9, A12, FUNCT_2:32
;
(P " ) . (x + y) =
(P " ) . (P . (x9 + y9))
by A5, A8, A11, GRCAT_1:def 13
.=
(P " ) . (P . (x9 + y9))
by A4, A3, TOPS_2:def 4
.=
((P " ) . x) + ((P " ) . y)
by A4, A9, A12, FUNCT_2:32
;
hence
(
(P " ) . (x + y) = ((P " ) . x) + ((P " ) . y) &
(P " ) . (x * y) = ((P " ) . x) * ((P " ) . y) &
(P " ) . (1_ S) = 1_ R )
by A13, A6;
verum
end;
then
( P " is additive & P " is multiplicative & P " is unity-preserving )
by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
then A14:
P " is RingHomomorphism
by QUOFIELD:def 21;
A15:
rng P = [#] S
by A2, QUOFIELD:def 22;
then rng (P " ) =
[#] R
by A4, TOPS_2:62
.=
the carrier of R
;
then A16:
P " is RingEpimorphism
by A14, QUOFIELD:def 22;
P " is one-to-one
by A4, A15, TOPS_2:63;
then
P " is RingMonomorphism
by A14, QUOFIELD:def 23;
hence
P " is RingIsomorphism
by A16, QUOFIELD:def 24; verum