let I be non empty set ; for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let J be non-empty disjoint_valued ManySortedSet of I; for G being Group
for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let G be Group; for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let M be Group-Family of I; for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let N be Group-Family of I,J; ( Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) implies M is DirectSumComponents of G,I )
assume that
A1:
Union N is DirectSumComponents of G, Union J
and
A2:
for i being Element of I holds N . i is DirectSumComponents of M . i,J . i
; M is DirectSumComponents of G,I
set UN = Union N;
consider fNtoG being Homomorphism of (sum (Union N)),G such that
A3:
fNtoG is bijective
by A1, GROUP_19:def 8;
deffunc H1( object ) -> set = the carrier of (sum (N . (In ($1,I))));
consider DS being Function such that
A4:
( dom DS = I & ( for i being object st i in I holds
DS . i = H1(i) ) )
from FUNCT_1:sch 3();
reconsider DS = DS as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;
deffunc H2( object ) -> set = the carrier of (M . (In ($1,I)));
consider RS being Function such that
A5:
( dom RS = I & ( for i being object st i in I holds
RS . i = H2(i) ) )
from FUNCT_1:sch 3();
reconsider RS = RS as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;
defpred S1[ object , object ] means ex fi being Homomorphism of (M . (In ($1,I))),(sum (N . (In ($1,I)))) st
( fi = $2 & fi is bijective );
A6:
for i being Element of I ex y being Element of PFuncs ((Union RS),(Union DS)) st S1[i,y]
proof
let i be
Element of
I;
ex y being Element of PFuncs ((Union RS),(Union DS)) st S1[i,y]
N . i is
DirectSumComponents of
M . i,
J . i
by A2;
then consider g being
Homomorphism of
(sum (N . i)),
(M . i) such that A7:
g is
bijective
by GROUP_19:def 8;
reconsider h =
g " as
Homomorphism of
(M . i),
(sum (N . i)) by A7, GROUP_6:62;
A8:
h is
bijective
by A7, GROUP_6:63;
A9:
In (
i,
I)
= i
;
(
DS . i in rng DS &
RS . i in rng RS )
by A4, A5, FUNCT_1:3;
then
( the
carrier of
(sum (N . i)) in rng DS & the
carrier of
(M . i) in rng RS )
by A4, A5, A9;
then
( the
carrier of
(sum (N . i)) c= Union DS & the
carrier of
(M . i) c= Union RS )
by ZFMISC_1:74;
then
(
dom h c= Union RS &
rng h c= Union DS )
;
then reconsider y =
h as
Element of
PFuncs (
(Union RS),
(Union DS))
by PARTFUN1:def 3;
take
y
;
S1[i,y]
thus
ex
h being
Homomorphism of
(M . (In (i,I))),
(sum (N . (In (i,I)))) st
(
h = y &
h is
bijective )
by A8;
verum
end;
consider fMtoBN being Function of I,(PFuncs ((Union RS),(Union DS))) such that
A10:
for i being Element of I holds S1[i,fMtoBN . i]
from FUNCT_2:sch 3(A6);
A11:
dom fMtoBN = I
by FUNCT_2:def 1;
reconsider fMtoBN = fMtoBN as ManySortedSet of I ;
reconsider fMtoDN = SumMap (M,(sum_bundle N),fMtoBN) as Homomorphism of (sum M),(dsum N) ;
for i being Element of I ex hi being Homomorphism of (M . i),((sum_bundle N) . i) st
( hi = fMtoBN . i & hi is bijective )
then A14:
fMtoDN is bijective
by A11, GROUP_19:41;
reconsider h = (fNtoG * (dsum2sum N)) * fMtoDN as Homomorphism of (sum M),G ;
take
h
; GROUP_19:def 8 h is bijective
A15:
( fNtoG * (dsum2sum N) is one-to-one & fNtoG * (dsum2sum N) is onto )
by A3, FUNCT_2:27;
( h is one-to-one & h is onto )
by A14, A15, FUNCT_2:27;
hence
h is bijective
; verum