let I be non empty set ; for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let F be Group-like associative multMagma-Family of I; for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let i be Element of I; ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
A1:
the carrier of (ProjGroup (F,i)) = ProjSet (F,i)
by Def2;
defpred S1[ set , set ] means $2 = (1_ (product F)) +* (i,$1);
A2:
for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S1[x,y]
consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that
A3:
for x being Element of the carrier of (F . i) holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
for a, b being Element of (F . i) holds f . (a * b) = (f . a) * (f . b)
proof
let a,
b be
Element of
(F . i);
f . (a * b) = (f . a) * (f . b)
A4:
f . a = (1_ (product F)) +* (
i,
a)
by A3;
A5:
f . b = (1_ (product F)) +* (
i,
b)
by A3;
A6:
f . (a * b) = (1_ (product F)) +* (
i,
(a * b))
by A3;
the
carrier of
(ProjGroup (F,i)) = ProjSet (
F,
i)
by Def2;
then reconsider ffa =
f . a,
ffb =
f . b as
Element of
(product F) by TARSKI:def 3;
thus (f . a) * (f . b) =
ffa * ffb
by GROUP_2:43
.=
f . (a * b)
by A6, A4, A5, Th3
;
verum
end;
then reconsider f = f as Homomorphism of (F . i),(ProjGroup (F,i)) by GROUP_6:def 6;
take
f
; ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
then A8:
the carrier of (ProjGroup (F,i)) c= rng f
by TARSKI:def 3;
rng f = the carrier of (ProjGroup (F,i))
by A8, XBOOLE_0:def 10;
then A9:
f is onto
by FUNCT_2:def 3;
for x1, x2 being object st x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 implies x1 = x2 )
assume A10:
(
x1 in the
carrier of
(F . i) &
x2 in the
carrier of
(F . i) &
f . x1 = f . x2 )
;
x1 = x2
then reconsider xx1 =
x1,
xx2 =
x2 as
Element of the
carrier of
(F . i) ;
A11:
f . xx1 = (1_ (product F)) +* (
i,
xx1)
by A3;
A12:
(1_ (product F)) +* (
i,
xx1)
= (1_ (product F)) +* (
i,
xx2)
by A10, A11, A3;
the
carrier of
(product F) = product (Carrier F)
by GROUP_7:def 2;
then A13:
dom (1_ (product F)) = I
by PARTFUN1:def 2;
thus x1 =
((1_ (product F)) +* (i .--> xx1)) . i
by FUNCT_7:94
.=
((1_ (product F)) +* (i,xx1)) . i
by A13, FUNCT_7:def 3
.=
((1_ (product F)) +* (i .--> xx2)) . i
by A13, A12, FUNCT_7:def 3
.=
x2
by FUNCT_7:94
;
verum
end;
then
f is one-to-one
by FUNCT_2:19;
hence
f is bijective
by A9; for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x)
thus
for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x)
by A3; verum