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:11;
reconsider x9 =
x9 as
Element of
R by A5;
B1:
f is
onto
by A2, FUNCT_2:def 3;
A7:
x9 =
(f ") . (f . x9)
by A3, FUNCT_2:26
.=
(f ") . x
by A3, A6, B1, 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:11;
reconsider y9 =
y9 as
Element of
R by A8;
A10:
y9 =
(f ") . (f . y9)
by A3, FUNCT_2:26
.=
(f ") . y
by A3, A9, B1, TOPS_2:def 4
;
thus (f ") . (x + y) =
(f ") . (f . (x9 + y9))
by A4, A6, A9, GRCAT_1:def 8
.=
(f ") . (f . (x9 + y9))
by B1, A3, TOPS_2:def 4
.=
((f ") . x) + ((f ") . y)
by A3, A7, A10, FUNCT_2:26
;
( (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 6
.=
(f ") . (f . (x9 * y9))
by B1, A3, TOPS_2:def 4
.=
((f ") . x) * ((f ") . y)
by A3, A7, A10, FUNCT_2:26
;
(f ") . (1_ S) = 1_ R
thus (f ") . (1_ S) =
(f ") . (f . (1_ R))
by A4, GROUP_1:def 13
.=
(f ") . (f . (1_ R))
by B1, A3, TOPS_2:def 4
.=
1_ R
by A3, FUNCT_2:26
;
verum
end;
then A11:
( f " is additive & f " is multiplicative & f " is unity-preserving )
by GRCAT_1:def 8, GROUP_1:def 13, GROUP_6:def 6;
A12:
rng f = [#] S
by A1, Def22;
then rng (f ") =
[#] R
by A3, TOPS_2:49
.=
the carrier of R
;
then A13:
f " is RingEpimorphism
by A11, Def22;
f " is one-to-one
by A3, A12, TOPS_2:50;
then
f " is RingMonomorphism
by A11, Def23;
hence
ex f being Function of S,R st f is RingIsomorphism
by A13; verum