let A be AbGroup; for X being non empty set
for f being Function of A,X st f is bijective holds
emb_AbGr f is AbGroup
let X be non empty set ; for f being Function of A,X st f is bijective holds
emb_AbGr f is AbGroup
let f be Function of A,X; ( f is bijective implies emb_AbGr f is AbGroup )
assume A1:
f is bijective
; emb_AbGr f is AbGroup
then A2:
rng f = X
by FUNCT_2:def 3;
A3:
dom f = [#] A
by FUNCT_2:def 1;
reconsider ZS = addLoopStr(# X,(addemb f),(f . (0. A)) #) as non empty addLoopStr ;
A5:
for v, w being Element of ZS holds v + w = w + v
proof
let v,
w be
Element of
ZS;
v + w = w + v
reconsider v1 =
v,
w1 =
w as
Element of
X ;
reconsider x =
(f ") . v1,
y =
(f ") . w1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
v + w =
addemb (
f,
v1,
w1)
by Def9
.=
f . (x + y)
by A1, Def8
.=
f . (y + x)
.=
addemb (
f,
w1,
v1)
by A1, Def8
.=
w + v
by Def9
;
hence
v + w = w + v
;
verum
end;
A6:
emb_AbGr f is Abelian
by A5;
A7:
for u, v, w being Element of ZS holds u + (v + w) = (u + v) + w
proof
let u,
v,
w be
Element of
ZS;
u + (v + w) = (u + v) + w
reconsider u1 =
u,
v1 =
v,
w1 =
w as
Element of
X ;
u + (v + w) =
addemb (
f,
u1,
((addemb f) . (v1,w1)))
by Def9
.=
addemb (
f,
u1,
(addemb (f,v1,w1)))
by Def9
.=
addemb (
f,
(addemb (f,u1,v1)),
w1)
by A1, Th11
.=
addemb (
f,
((addemb f) . (u1,v1)),
w1)
by Def9
.=
(u + v) + w
by Def9
;
hence
u + (v + w) = (u + v) + w
;
verum
end;
A8:
emb_AbGr f is add-associative
by A7;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be
Element of
ZS;
v + (0. ZS) = v
reconsider v1 =
v as
Element of
X ;
reconsider x =
(f ") . v1 as
Element of
[#] A by A2, A3, A1, FUNCT_1:32;
v + (0. ZS) =
addemb (
f,
v1,
(f . (0. A)))
by Def9
.=
f . ( the addF of A . (((f ") . v1),((f ") . (f . (0. A)))))
by A1, Def8
.=
f . (x + (0. A))
by A1, A3, FUNCT_1:34
.=
v1
by A1, A2, FUNCT_1:35
;
hence
v + (0. ZS) = v
;
verum
end;
then A9:
emb_AbGr f is right_zeroed
;
A10:
for v being Element of ZS holds v is right_complementable
proof
let v be
Element of
ZS;
v is right_complementable
reconsider v1 =
v as
Element of
X ;
reconsider x =
(f ") . v1 as
Element of
A by A2, A3, A1, FUNCT_1:32;
consider u being
Element of
ZS such that A11:
u = f . (- x)
;
reconsider u1 =
u as
Element of
X ;
v + u =
addemb (
f,
v1,
u1)
by Def9
.=
f . ( the addF of A . (((f ") . v1),((f ") . u1)))
by A1, Def8
.=
f . (x + (- x))
by A11, A3, A1, FUNCT_1:34
.=
0. ZS
by RLVECT_1:5
;
hence
v is
right_complementable
;
verum
end;
emb_AbGr f is right_complementable
by A10;
hence
emb_AbGr f is AbGroup
by A6, A8, A9; verum