let A be comRing; for X being non empty set
for f being Function of A,X st f is bijective holds
emb_Ring f is comRing
let X be non empty set ; for f being Function of A,X st f is bijective holds
emb_Ring f is comRing
let f be Function of A,X; ( f is bijective implies emb_Ring f is comRing )
assume A1:
f is bijective
; emb_Ring f is comRing
then A2:
rng f = X
by FUNCT_2:def 3;
A3:
dom f = [#] A
by FUNCT_2:def 1;
reconsider ZS = doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #) as non empty doubleLoopStr ;
emb_Ring f is commutative
proof
for
a,
b,
v being
Element of
ZS holds
a * b = b * a
proof
let a,
b be
Element of
ZS;
for v being Element of ZS holds a * b = b * a
reconsider a1 =
a,
b1 =
b as
Element of
X ;
reconsider x =
(f ") . a1,
y =
(f ") . b1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
reconsider ab1 =
a * b as
Element of
X ;
a * b =
multemb (
f,
a1,
b1)
by Def4
.=
f . (x * y)
by A1, Def3
.=
f . (y * x)
.=
multemb (
f,
b1,
a1)
by A1, Def3
.=
b * a
by Def4
;
hence
for
v being
Element of
ZS holds
a * b = b * a
;
verum
end;
hence
emb_Ring f is
commutative
;
verum
end;
hence
emb_Ring f is comRing
by A1, Th6; verum