let I be non empty set ; for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let J be non-empty disjoint_valued ManySortedSet of I; for G being Group
for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let G be Group; for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let M be DirectSumComponents of G,I; for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let N be Group-Family of I,J; ( ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) implies Union N is DirectSumComponents of G, Union J )
assume A1:
for i being Element of I holds N . i is DirectSumComponents of M . i,J . i
; Union N is DirectSumComponents of G, Union J
consider fM2G being Homomorphism of (sum M),G such that
A2:
fM2G is bijective
by GROUP_19:def 8;
deffunc H1( object ) -> Element of bool the carrier of (sum (N . (In ($1,I)))) = [#] (sum (N . (In ($1,I))));
consider DS being Function such that
A3:
( 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 A3, PARTFUN1:def 2, RELAT_1:def 18;
deffunc H2( object ) -> Element of bool the carrier of (M . (In ($1,I))) = [#] (M . (In ($1,I)));
consider RS being Function such that
A4:
( 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 A4, PARTFUN1:def 2, RELAT_1:def 18;
defpred S1[ object , object ] means ex fi being Homomorphism of (sum (N . (In ($1,I)))),(M . (In ($1,I))) st
( fi = $2 & fi is bijective );
A5:
for i being Element of I ex y being Element of PFuncs ((Union DS),(Union RS)) st S1[i,y]
proof
let i be
Element of
I;
ex y being Element of PFuncs ((Union DS),(Union RS)) st S1[i,y]
N . i is
DirectSumComponents of
M . i,
J . i
by A1;
then consider h being
Homomorphism of
(sum (N . i)),
(M . i) such that A6:
h is
bijective
by GROUP_19:def 8;
A7:
In (
i,
I)
= i
;
(
DS . i = [#] (sum (N . i)) &
RS . i = [#] (M . i) )
by A3, A4, A7;
then
(
[#] (sum (N . i)) c= Union DS &
[#] (M . i) c= Union RS )
by A3, A4, FUNCT_1:3, ZFMISC_1:74;
then
(
dom h c= Union DS &
rng h c= Union RS )
;
then reconsider y =
h as
Element of
PFuncs (
(Union DS),
(Union RS))
by PARTFUN1:def 3;
take
y
;
S1[i,y]
thus
S1[
i,
y]
by A6;
verum
end;
consider fBN2M being Function of I,(PFuncs ((Union DS),(Union RS))) such that
A9:
for i being Element of I holds S1[i,fBN2M . i]
from FUNCT_2:sch 3(A5);
reconsider fBN2M = fBN2M as ManySortedSet of I ;
set fDN2M = ProductHom (G,M,N,fBN2M);
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = fBN2M . i & hi is bijective )
then A12:
ProductHom (G,M,N,fBN2M) is bijective
by Def16;
reconsider h = (fM2G * (ProductHom (G,M,N,fBN2M))) * (sum2dsum N) as Homomorphism of (sum (Union N)),G ;
take
h
; GROUP_19:def 8 h is bijective
( fM2G * (ProductHom (G,M,N,fBN2M)) is one-to-one & fM2G * (ProductHom (G,M,N,fBN2M)) is onto )
by A2, A12, FUNCT_2:27;
then
( h is one-to-one & h is onto )
by FUNCT_2:27;
hence
h is bijective
; verum