let I be non empty set ; for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being Subgroup-Family of I,G
for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
M is internal DirectSumComponents of G,I
let J be non-empty disjoint_valued ManySortedSet of I; for G being Group
for M being Subgroup-Family of I,G
for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
M is internal DirectSumComponents of G,I
let G be Group; for M being Subgroup-Family of I,G
for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
M is internal DirectSumComponents of G,I
let M be Subgroup-Family of I,G; for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
M is internal DirectSumComponents of G,I
let N be Group-Family of I,J; ( Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) implies M is internal DirectSumComponents of G,I )
assume that
A1:
Union N is internal DirectSumComponents of G, Union J
and
A2:
for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i
; M is internal DirectSumComponents of G,I
reconsider UJ = Union J as non empty set ;
for i being Element of I holds N . i is DirectSumComponents of M . i,J . i
by A2;
then reconsider M = M as DirectSumComponents of G,I by A1, Th41;
A3:
dom J = I
by PARTFUN1:def 2;
consider fNtoG being Homomorphism of (sum (Union N)),G such that
A4:
fNtoG is bijective
and
A5:
for x being finite-support Function of UJ,G st x in sum (Union N) holds
fNtoG . x = Product x
by A1, GROUP_19:def 9;
defpred S1[ object , object ] means ex Ni being internal DirectSumComponents of M . (In ($1,I)),J . (In ($1,I)) st
( Ni = N . $1 & $2 = (InterHom Ni) " );
A6:
for x, y1, y2 being object st x in I & S1[x,y1] & S1[x,y2] holds
y1 = y2
;
A7:
for x being object st x in I holds
ex y being object st S1[x,y]
consider fMtoBN being Function such that
A9:
( dom fMtoBN = I & ( for i being object st i in I holds
S1[i,fMtoBN . i] ) )
from FUNCT_1:sch 2(A6, A7);
reconsider fMtoBN = fMtoBN as ManySortedSet of I by A9, PARTFUN1:def 2, RELAT_1:def 18;
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 )
proof
let i be
Element of
I;
ex hi being Homomorphism of (M . i),((sum_bundle N) . i) st
( hi = fMtoBN . i & hi is bijective )
consider Ni being
internal DirectSumComponents of
M . (In (i,I)),
J . (In (i,I)) such that A11:
(
Ni = N . i &
fMtoBN . i = (InterHom Ni) " )
by A9;
reconsider g =
InterHom Ni as
Homomorphism of
(sum (N . i)),
(M . i) by A11;
reconsider fi =
g " as
Homomorphism of
(M . i),
(sum (N . i)) by A11, Def15, GROUP_6:62;
g is
bijective
by A11, Def15;
then A12:
(
fi = fMtoBN . i &
fi is
bijective )
by A11, GROUP_6:63;
sum (N . (In (i,I))) = (sum_bundle N) . i
by Def7;
hence
ex
hi being
Homomorphism of
(M . i),
((sum_bundle N) . i) st
(
hi = fMtoBN . i &
hi is
bijective )
by A12;
verum
end;
then A13:
fMtoDN is bijective
by A9, GROUP_19:41;
reconsider h = (fNtoG * (dsum2sum N)) * fMtoDN as Homomorphism of (sum M),G ;
A14:
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi " = fMtoBN . i & hi is bijective & ( for x being finite-support Function of (J . i),(M . i) st x in (sum_bundle N) . i holds
hi . x = Product x ) )
proof
let i be
Element of
I;
ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi " = fMtoBN . i & hi is bijective & ( for x being finite-support Function of (J . i),(M . i) st x in (sum_bundle N) . i holds
hi . x = Product x ) )
consider Ni being
internal DirectSumComponents of
M . (In (i,I)),
J . (In (i,I)) such that A16:
(
Ni = N . i &
fMtoBN . i = (InterHom Ni) " )
by A9;
A17:
(
InterHom Ni is
bijective & ( for
x being
finite-support Function of
(J . i),
(M . i) st
x in sum Ni holds
(InterHom Ni) . x = Product x ) )
by Def15;
A18:
sum (N . (In (i,I))) = (sum_bundle N) . i
by Def7;
then reconsider hi =
InterHom Ni as
Homomorphism of
((sum_bundle N) . i),
(M . i) by A16;
thus
ex
hi being
Homomorphism of
((sum_bundle N) . i),
(M . i) st
(
hi " = fMtoBN . i &
hi is
bijective & ( for
x being
finite-support Function of
(J . i),
(M . i) st
x in (sum_bundle N) . i holds
hi . x = Product x ) )
by A16, A17, A18;
verum
end;
A19:
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi " = fMtoBN . i & hi is bijective )
( fNtoG * (dsum2sum N) is one-to-one & fNtoG * (dsum2sum N) is onto )
by A4, FUNCT_2:27;
then A21:
( h is one-to-one & h is onto )
by A13, FUNCT_2:27;
for i being Element of I holds N . i is DirectSumComponents of M . i,J . i
by A2;
then reconsider UN = Union N as DirectSumComponents of G,UJ by Th39;
reconsider UJ = Union J as non empty set ;
A22:
for j being object st j in UJ holds
UN . j is Subgroup of G
by A1, GROUP_19:def 9;
A23:
for i being Element of I holds M . i is Subgroup of G
by GROUP_20:def 1;
reconsider UN = UN as Subgroup-Family of UJ,G by A22, GROUP_20:def 1;
for x being finite-support Function of I,G st x in sum M holds
h . x = Product x
proof
let x be
finite-support Function of
I,
G;
( x in sum M implies h . x = Product x )
assume A24:
x in sum M
;
h . x = Product x
for
i being
Element of
I for
g being
Element of
(M . i) holds
h . ((1ProdHom (M,i)) . g) = g
proof
let i be
Element of
I;
for g being Element of (M . i) holds h . ((1ProdHom (M,i)) . g) = glet g be
Element of
(M . i);
h . ((1ProdHom (M,i)) . g) = g
A25:
dom (dsum2sum N) = the
carrier of
(dsum N)
by FUNCT_2:def 1;
A26:
(1ProdHom (M,i)) . g in ProjGroup (
M,
i)
;
then A27:
(1ProdHom (M,i)) . g in sum M
by GROUP_2:40;
then
(1ProdHom (M,i)) . g in dom fMtoDN
by FUNCT_2:def 1;
then A28:
h . ((1ProdHom (M,i)) . g) = (fNtoG * (dsum2sum N)) . (fMtoDN . ((1ProdHom (M,i)) . g))
by FUNCT_1:13;
A29:
fMtoDN . ((1ProdHom (M,i)) . g) in the
carrier of
(dsum N)
by A27, FUNCT_2:5;
A30:
(fNtoG * (dsum2sum N)) . (fMtoDN . ((1ProdHom (M,i)) . g)) = fNtoG . ((dsum2sum N) . (fMtoDN . ((1ProdHom (M,i)) . g)))
by A27, FUNCT_2:5, FUNCT_2:15;
A31:
(dsum2sum N) . (fMtoDN . ((1ProdHom (M,i)) . g)) in sum UN
by A29, FUNCT_2:5;
for
j being
object st
j in UJ holds
UN . j is
Subgroup of
G
by A1, GROUP_19:def 9;
then reconsider z =
(dsum2sum N) . (fMtoDN . ((1ProdHom (M,i)) . g)) as
finite-support Function of
UJ,
G by A31, GROUP_19:10;
A32:
(fNtoG * (dsum2sum N)) . (fMtoDN . ((1ProdHom (M,i)) . g)) = Product z
by A5, A30, A31;
A33:
(dsum2sum N) . (fMtoDN . ((1ProdHom (M,i)) . g)) = (dprod2prod N) . (fMtoDN . ((1ProdHom (M,i)) . g))
by A25, A27, FUNCT_1:47, FUNCT_2:5;
(1ProdHom (M,i)) . g in product M
by A26, GROUP_2:40;
then reconsider y =
(1ProdHom (M,i)) . g as
Element of
(product M) ;
fMtoDN . ((1ProdHom (M,i)) . g) in dsum N
by A27, FUNCT_2:5;
then
fMtoDN . ((1ProdHom (M,i)) . g) in dprod N
by GROUP_2:40;
then reconsider t =
fMtoDN . ((1ProdHom (M,i)) . g) as
Element of
(dprod N) ;
A34:
for
k being
Element of
I holds
t . k = z | (J . k)
by A33, Def10;
A35:
for
i being
Element of
I holds
fMtoBN . i is
Homomorphism of
(M . i),
((sum_bundle N) . i)
consider hi being
Homomorphism of
((sum_bundle N) . i),
(M . i) such that A37:
(
hi " = fMtoBN . i &
hi is
bijective & ( for
x being
finite-support Function of
(J . i),
(M . i) st
x in (sum_bundle N) . i holds
hi . x = Product x ) )
by A14;
A38:
(
hi is
one-to-one &
rng hi = the
carrier of
(M . i) )
by A37, FUNCT_2:def 3;
then A39:
hi " is
Function of the
carrier of
(M . i), the
carrier of
((sum_bundle N) . i)
by FUNCT_2:25;
A40:
hi " is
Homomorphism of
(M . i),
((sum_bundle N) . i)
by A37, GROUP_6:62;
A41:
fMtoDN . ((1ProdHom (M,i)) . g) = (1ProdHom ((sum_bundle N),i)) . ((hi ") . g)
by A9, A35, A37, A40, GROUP_19:42;
reconsider hkg =
(hi ") . g as
Element of
((sum_bundle N) . i) by A39, FUNCT_2:5;
(1ProdHom ((sum_bundle N),i)) . hkg in ProjGroup (
(sum_bundle N),
i)
;
then
(1ProdHom ((sum_bundle N),i)) . hkg in product (sum_bundle N)
by GROUP_2:40;
then reconsider p =
(1ProdHom ((sum_bundle N),i)) . hkg as
Function ;
A42:
(hi ") . g in (sum_bundle N) . i
by A39, FUNCT_2:5;
then A43:
(hi ") . g in sum (N . i)
by Def7;
then reconsider hkg0 =
(hi ") . g as
Function ;
for
j being
object st
j in J . i holds
(N . i) . j is
Subgroup of
G
then reconsider hkg0 =
hkg0 as
finite-support Function of
(J . i),
G by A43, GROUP_19:10;
J . i c= Union J
by A3, FUNCT_1:3, ZFMISC_1:74;
then A46:
J . i c= UJ
;
A47:
p . i = z | (J . i)
by A34, A41;
A48:
p = (1_ (product (sum_bundle N))) +* (
i,
hkg)
by GROUP_12:def 3;
A49:
dom (1_ (product (sum_bundle N))) = I
by GROUP_19:3;
then A50:
z | (J . i) = hkg0
by A47, A48, FUNCT_7:31;
for
m being
object holds
(
m in support z iff
m in support hkg0 )
proof
let m be
object ;
( m in support z iff m in support hkg0 )
hereby ( m in support hkg0 implies m in support z )
assume QX:
m in support z
;
m in support hkg0then A51:
(
z . m <> 1_ G &
m in UJ )
by GROUP_19:def 2;
then consider Y being
set such that A52:
(
m in Y &
Y in rng J )
by TARSKI:def 4;
consider k being
object such that A53:
(
k in dom J &
Y = J . k )
by A52, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A53;
A54:
k = i
proof
assume A55:
k <> i
;
contradiction
UN . m = (N . k) . m
by A52, A53, Th19;
then reconsider P =
(N . k) . m as
Subgroup of
G by A1, GROUP_19:def 9, QX;
p . k =
1_ ((sum_bundle N) . k)
by A48, A55, GROUP_12:1
.=
1_ (sum (N . k))
by Def7
;
then (z | (J . k)) . m =
(1_ (sum (N . k))) . m
by A34, A41
.=
(1_ (product (N . k))) . m
by GROUP_2:44
.=
1_ P
by A52, A53, GROUP_7:6
.=
1_ G
by GROUP_2:44
;
hence
contradiction
by A51, A52, A53, FUNCT_1:49;
verum
end; then z . m =
(z | (J . i)) . m
by A52, A53, FUNCT_1:49
.=
hkg0 . m
by A47, A48, A49, FUNCT_7:31
;
hence
m in support hkg0
by A51, A52, A53, A54, GROUP_19:def 2;
verum
end;
assume
m in support hkg0
;
m in support z
then A57:
(
hkg0 . m <> 1_ G &
m in J . i )
by GROUP_19:def 2;
z . m <> 1_ G
by A50, A57, FUNCT_1:49;
hence
m in support z
by A46, A57, GROUP_19:def 2;
verum
end;
then A58:
support z = support hkg0
by TARSKI:2;
for
j being
object st
j in J . i holds
(N . i) . j is
Subgroup of
M . i
then reconsider hkg01 =
hkg0 as
finite-support Function of
(J . i),
(M . i) by A43, GROUP_19:10;
A60:
M . i is
Subgroup of
G
by GROUP_20:def 1;
g =
hi . ((hi ") . g)
by A38, FUNCT_1:35
.=
Product hkg01
by A37, A42
.=
Product hkg0
by A60, GROUP_20:6
;
hence
h . ((1ProdHom (M,i)) . g) = g
by A28, A32, A50, A58, RELAT_1:74;
verum
end;
hence
h . x = Product x
by A24, GROUP_20:18;
verum
end;
hence
M is internal DirectSumComponents of G,I
by A21, A23, GROUP_19:def 9; verum