let R, S be non empty doubleLoopStr ; :: thesis: ( ex f being Function of R,S st f is RingIsomorphism implies ex f being Function of S,R st f is RingIsomorphism )
given f being Function of R,S such that A1:
f is RingIsomorphism
; :: thesis: ex f being Function of S,R st f is RingIsomorphism
A2:
( f is RingMonomorphism & f is RingEpimorphism )
by A1;
then A3:
( f is RingHomomorphism & f is one-to-one & rng f = the carrier of S )
by Def22, Def23;
then A4:
( f is additive & f is multiplicative & f is unity-preserving )
;
A5:
rng f = [#] S
by A2, Def22;
set g = f " ;
A6:
f " is RingHomomorphism
proof
for
x,
y being
Element of
S holds
(
(f " ) . (x + y) = ((f " ) . x) + ((f " ) . y) &
(f " ) . (x * y) = ((f " ) . x) * ((f " ) . y) &
(f " ) . (1_ S) = 1_ R )
proof
let x,
y be
Element of
S;
:: thesis: ( (f " ) . (x + y) = ((f " ) . x) + ((f " ) . y) & (f " ) . (x * y) = ((f " ) . x) * ((f " ) . y) & (f " ) . (1_ S) = 1_ R )
consider x' being
set such that A7:
(
x' in the
carrier of
R &
f . x' = x )
by A3, FUNCT_2:17;
reconsider x' =
x' as
Element of
R by A7;
consider y' being
set such that A8:
(
y' in the
carrier of
R &
f . y' = y )
by A3, FUNCT_2:17;
reconsider y' =
y' as
Element of
R by A8;
A9:
x' =
(f " ) . (f . x')
by A3, FUNCT_2:32
.=
(f " ) . x
by A3, A7, TOPS_2:def 4
;
A10:
y' =
(f " ) . (f . y')
by A3, FUNCT_2:32
.=
(f " ) . y
by A3, A8, TOPS_2:def 4
;
thus (f " ) . (x + y) =
(f " ) . (f . (x' + y'))
by A4, A7, A8, GRCAT_1:def 13
.=
(f " ) . (f . (x' + y'))
by A3, TOPS_2:def 4
.=
((f " ) . x) + ((f " ) . y)
by A3, A9, A10, FUNCT_2:32
;
:: thesis: ( (f " ) . (x * y) = ((f " ) . x) * ((f " ) . y) & (f " ) . (1_ S) = 1_ R )
thus (f " ) . (x * y) =
(f " ) . (f . (x' * y'))
by A4, A7, A8, GROUP_6:def 7
.=
(f " ) . (f . (x' * y'))
by A3, TOPS_2:def 4
.=
((f " ) . x) * ((f " ) . y)
by A3, A9, A10, FUNCT_2:32
;
:: thesis: (f " ) . (1_ S) = 1_ R
thus (f " ) . (1_ S) =
(f " ) . (f . (1_ R))
by A4, GROUP_1:def 17
.=
(f " ) . (f . (1_ R))
by A3, TOPS_2:def 4
.=
1_ R
by A3, FUNCT_2:32
;
:: thesis: verum
end;
then
(
f " is
additive &
f " is
multiplicative &
f " is
unity-preserving )
by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence
f " is
RingHomomorphism
;
:: thesis: verum
end;
f " is one-to-one
by A3, A5, TOPS_2:63;
then A11:
f " is RingMonomorphism
by A6, Def23;
rng (f " ) =
[#] R
by A3, A5, TOPS_2:62
.=
the carrier of R
;
then
f " is RingEpimorphism
by A6, Def22;
then
f " is RingIsomorphism
by A11;
hence
ex f being Function of S,R st f is RingIsomorphism
; :: thesis: verum