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