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