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:
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;
:: 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 A5:
x' in the
carrier of
R
and A6:
f . x' = x
by A2, FUNCT_2:17;
reconsider x' =
x' as
Element of
R by A5;
A7:
x' =
(f " ) . (f . x')
by A3, FUNCT_2:32
.=
(f " ) . x
by A3, A2, A6, TOPS_2:def 4
;
consider y' being
set such that A8:
y' in the
carrier of
R
and A9:
f . y' = y
by A2, FUNCT_2:17;
reconsider y' =
y' as
Element of
R by A8;
A10:
y' =
(f " ) . (f . y')
by A3, FUNCT_2:32
.=
(f " ) . y
by A3, A2, A9, TOPS_2:def 4
;
thus (f " ) . (x + y) =
(f " ) . (f . (x' + y'))
by A4, A6, A9, GRCAT_1:def 13
.=
(f " ) . (f . (x' + y'))
by A3, A2, TOPS_2:def 4
.=
((f " ) . x) + ((f " ) . y)
by A3, A7, 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, A6, A9, GROUP_6:def 7
.=
(f " ) . (f . (x' * y'))
by A3, A2, TOPS_2:def 4
.=
((f " ) . x) * ((f " ) . y)
by A3, A7, 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, A2, TOPS_2:def 4
.=
1_ R
by A3, FUNCT_2:32
;
:: thesis: 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; :: thesis: verum