let I be non empty set ; for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being internal DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J
let J be non-empty disjoint_valued ManySortedSet of I; for G being Group
for M being internal DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J
let G be Group; for M being internal DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J
let M be internal DirectSumComponents of G,I; for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J
let N be Group-Family of I,J; ( ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) implies Union N is internal DirectSumComponents of G, Union J )
assume A1:
for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i
; Union N is internal DirectSumComponents of G, Union J
A2:
dom J = I
by PARTFUN1:def 2;
consider fMtoG being Homomorphism of (sum M),G such that
A3:
fMtoG is bijective
and
A4:
for x being finite-support Function of I,G st x in sum M holds
fMtoG . x = Product x
by 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 );
A5:
for i, f1, f2 being object st i in I & S1[i,f1] & S1[i,f2] holds
f1 = f2
;
A6:
for x being object st x in I holds
ex y being object st S1[x,y]
consider fBNtoM being Function such that
A8:
( dom fBNtoM = I & ( for i being object st i in I holds
S1[i,fBNtoM . i] ) )
from FUNCT_1:sch 2(A5, A6);
reconsider fBNtoM = fBNtoM as ManySortedSet of I by A8, PARTFUN1:def 2, RELAT_1:def 18;
set fDNtoM = ProductHom (G,M,N,fBNtoM);
A9:
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = fBNtoM . 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 = fBNtoM . 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 A11:
(
Ni = N . i &
fBNtoM . i = InterHom Ni )
by A8;
A12:
(
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;
A13:
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 A11;
take
hi
;
( hi = fBNtoM . 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 ) )
thus
hi = fBNtoM . i
by A11;
( 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 ) )
thus
hi is
bijective
by A12;
for x being finite-support Function of (J . i),(M . i) st x in (sum_bundle N) . i holds
hi . x = Product x
thus
for
x being
finite-support Function of
(J . i),
(M . i) st
x in (sum_bundle N) . i holds
hi . x = Product x
by A11, A13, Def15;
verum
end;
A14:
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = fBNtoM . i & hi is bijective )
A16:
ProductHom (G,M,N,fBNtoM) is bijective
by A14, Def16;
reconsider h = (fMtoG * (ProductHom (G,M,N,fBNtoM))) * (sum2dsum N) as Homomorphism of (sum (Union N)),G ;
( fMtoG * (ProductHom (G,M,N,fBNtoM)) is one-to-one & fMtoG * (ProductHom (G,M,N,fBNtoM)) is onto )
by A3, A16, FUNCT_2:27;
then A18:
( h is one-to-one & h is onto )
by FUNCT_2:27;
A19:
for i being Element of I holds N . i is DirectSumComponents of M . i,J . i
by A1;
reconsider UJ = Union J as non empty set ;
reconsider UN = Union N as DirectSumComponents of G,UJ by A19, Th39;
A20:
for i being Element of I holds M . i is Subgroup of G
by GROUP_19:def 9;
A21:
for j being object st j in UJ holds
UN . j is Subgroup of G
then A26:
for j being Element of UJ holds UN . j is Subgroup of G
;
reconsider UN = UN as Subgroup-Family of UJ,G by A21, GROUP_20:def 1;
for x being finite-support Function of UJ,G st x in sum UN holds
h . x = Product x
proof
let x be
finite-support Function of
UJ,
G;
( x in sum UN implies h . x = Product x )
assume A27:
x in sum UN
;
h . x = Product x
for
j being
Element of
UJ for
g being
Element of
(UN . j) holds
h . ((1ProdHom (UN,j)) . g) = g
proof
let j be
Element of
UJ;
for g being Element of (UN . j) holds h . ((1ProdHom (UN,j)) . g) = glet g be
Element of
(UN . j);
h . ((1ProdHom (UN,j)) . g) = g
UN . j is
Subgroup of
G
by A21;
then A28:
g is
Element of
G
by GROUP_2:42;
A29:
(1ProdHom (UN,j)) . g in ProjGroup (
UN,
j)
;
then A30:
(1ProdHom (UN,j)) . g in sum UN
by GROUP_2:40;
then A31:
(1ProdHom (UN,j)) . g in dom (sum2dsum N)
by FUNCT_2:def 1;
then A32:
h . ((1ProdHom (UN,j)) . g) = (fMtoG * (ProductHom (G,M,N,fBNtoM))) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g))
by FUNCT_1:13;
A33:
(sum2dsum N) . ((1ProdHom (UN,j)) . g) in [#] (dsum N)
by A30, FUNCT_2:5;
A34:
(fMtoG * (ProductHom (G,M,N,fBNtoM))) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g)) = fMtoG . ((ProductHom (G,M,N,fBNtoM)) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g)))
by A30, FUNCT_2:5, FUNCT_2:15;
A35:
(ProductHom (G,M,N,fBNtoM)) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g)) in sum M
by A33, FUNCT_2:5;
for
i being
object st
i in I holds
M . i is
Subgroup of
G
by GROUP_19:def 9;
then reconsider z =
(ProductHom (G,M,N,fBNtoM)) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g)) as
finite-support Function of
I,
G by A35, GROUP_19:10;
A36:
(fMtoG * (ProductHom (G,M,N,fBNtoM))) . ((sum2dsum N) . ((1ProdHom (UN,j)) . g)) = Product z
by A4, A34, A35;
consider Y being
set such that A37:
(
j in Y &
Y in rng J )
by TARSKI:def 4;
consider k being
object such that A38:
(
k in dom J &
Y = J . k )
by A37, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A38;
A39:
UN . j = (N . k) . j
by A37, A38, Th19;
N . k is
internal DirectSumComponents of
M . k,
J . k
by A1;
then reconsider K =
(N . k) . j as
Subgroup of
M . k by A37, A38, GROUP_19:def 9;
A41:
g in K
by A39;
A42:
sum2dsum N = (prod2dprod N) | (sum (Union N))
by Th36;
A43:
(sum2dsum N) . ((1ProdHom (UN,j)) . g) = (prod2dprod N) . ((1ProdHom (UN,j)) . g)
by A31, A42, FUNCT_1:47;
(1ProdHom (UN,j)) . g in product UN
by A29, GROUP_2:40;
then reconsider y =
(1ProdHom (UN,j)) . g as
Element of
(product (Union N)) ;
reconsider t =
(sum2dsum N) . ((1ProdHom (UN,j)) . g) as
Element of
(dsum N) by A30, FUNCT_2:5;
A44:
for
i being
Element of
I holds
fBNtoM . i is
Homomorphism of
((sum_bundle N) . i),
(M . i)
consider hk being
Homomorphism of
((sum_bundle N) . k),
(M . k) such that A45:
(
hk = fBNtoM . k &
hk is
bijective & ( for
x being
finite-support Function of
(J . k),
(M . k) st
x in (sum_bundle N) . k holds
hk . x = Product x ) )
by A9;
A46:
(
hk is
one-to-one &
rng hk = [#] (M . k) )
by A45, FUNCT_2:def 3;
then A47:
hk " is
Function of
([#] (M . k)),
([#] ((sum_bundle N) . k))
by FUNCT_2:25;
A48:
g in M . k
by A41, GROUP_2:40;
then
(hk ") . g is
Element of
((sum_bundle N) . k)
by A47, FUNCT_2:5;
then
(SumMap ((sum_bundle N),M,fBNtoM)) . ((1ProdHom ((sum_bundle N),k)) . ((hk ") . g)) = (1ProdHom (M,k)) . (hk . ((hk ") . g))
by A8, A44, A45, GROUP_19:42;
then A49:
(ProductHom (G,M,N,fBNtoM)) . ((1ProdHom ((sum_bundle N),k)) . ((hk ") . g)) =
(1ProdHom (M,k)) . (hk . ((hk ") . g))
by A14, Def16
.=
(1ProdHom (M,k)) . g
by A46, A48, FUNCT_1:35
;
reconsider hkg =
(hk ") . g as
Element of
((sum_bundle N) . k) by A47, A48, FUNCT_2:5;
A50:
(1ProdHom ((sum_bundle N),k)) . hkg in ProjGroup (
(sum_bundle N),
k)
;
then A51:
(1ProdHom ((sum_bundle N),k)) . hkg in product (sum_bundle N)
by GROUP_2:40;
then reconsider p =
(1ProdHom ((sum_bundle N),k)) . hkg as
Function ;
A52:
t in sum (sum_bundle N)
;
then
t in product (sum_bundle N)
by GROUP_2:40;
then A53:
dom t = I
by GROUP_19:3;
for
i being
object st
i in dom p holds
p . i = t . i
proof
let i0 be
object ;
( i0 in dom p implies p . i0 = t . i0 )
assume
i0 in dom p
;
p . i0 = t . i0
then reconsider i =
i0 as
Element of
I by A51, GROUP_19:3;
reconsider yi =
y | (J . i) as
Function ;
p . i in (sum_bundle N) . i
by A50, GROUP_2:40, GROUP_19:5;
then A54:
p . i in sum (N . i)
by Def7;
then A55:
p . i in product (N . i)
by GROUP_2:40;
reconsider xi =
p . i as
Function by A54;
y | (J . i) = t . i
by A43, Th25;
then
yi in (sum_bundle N) . i
by A52, GROUP_2:40, GROUP_19:5;
then
yi in sum (N . i)
by Def7;
then A56:
yi in product (N . i)
by GROUP_2:40;
then A57:
dom yi = J . i
by GROUP_19:3;
A58:
p = (1_ (product (sum_bundle N))) +* (
k,
hkg)
by GROUP_12:def 3;
A59:
y = (1_ (product UN)) +* (
j,
g)
by GROUP_12:def 3;
per cases
( i <> k or i = k )
;
suppose A60:
i <> k
;
p . i0 = t . i0then
xi = 1_ ((sum_bundle N) . i)
by A58, GROUP_12:1;
then A61:
xi = 1_ (sum (N . i))
by Def7;
for
n being
object st
n in dom yi holds
yi . n = xi . n
proof
let n0 be
object ;
( n0 in dom yi implies yi . n0 = xi . n0 )
assume A62:
n0 in dom yi
;
yi . n0 = xi . n0
then reconsider n =
n0 as
Element of
J . i by A56, GROUP_19:3;
(J . i) /\ (J . k) = {}
by A60, PROB_2:def 2, XBOOLE_0:def 7;
then A63:
j <> n
by A37, A38, XBOOLE_0:def 4;
J . i c= Union J
by A2, FUNCT_1:3, ZFMISC_1:74;
then reconsider n1 =
n as
Element of
UJ ;
thus yi . n0 =
y . n
by A62, FUNCT_1:47
.=
1_ (UN . n1)
by A59, A63, GROUP_12:1
.=
1_ ((N . i) . n)
by Th19
.=
(1_ (product (N . i))) . n
by GROUP_7:6
.=
xi . n0
by A61, GROUP_2:44
;
verum
end; then
yi = xi
by A55, A57, GROUP_19:3;
hence
p . i0 = t . i0
by A43, Th25;
verum end; suppose A65:
i = k
;
p . i0 = t . i0then A66:
xi = hkg
by A58, GROUP_12:1;
for
n being
object st
n in dom yi holds
yi . n = xi . n
proof
let n0 be
object ;
( n0 in dom yi implies yi . n0 = xi . n0 )
assume A67:
n0 in dom yi
;
yi . n0 = xi . n0
then reconsider n =
n0 as
Element of
J . i by A56, GROUP_19:3;
J . i c= Union J
by A2, FUNCT_1:3, ZFMISC_1:74;
then reconsider n1 =
n as
Element of
UJ ;
A69:
g is
Element of
K
by A37, A38, Th19;
1_ (sum (N . k)) in sum (N . k)
;
then A70:
(1_ (sum (N . k))) +* (
j,
g)
in sum (N . k)
by A37, A38, A69, GROUP_19:25;
then A71:
(1_ (sum (N . k))) +* (
j,
g)
in (sum_bundle N) . k
by Def7;
then
(1_ (sum (N . k))) +* (
j,
g)
in dom hk
by FUNCT_2:def 1;
then A72:
(1_ (product (N . k))) +* (
j,
g)
in dom hk
by GROUP_2:44;
A73:
N . k is
internal DirectSumComponents of
M . k,
J . k
by A1;
then A74:
for
j being
Element of
J . k holds
(N . k) . j is
Subgroup of
M . k
by GROUP_19:def 9;
A75:
1_ (product (N . k)) = (J . k) --> (1_ (M . k))
by A74, GROUP_19:13;
set q =
((J . k) --> (1_ (M . k))) +* (
j,
g);
A76:
((J . k) --> (1_ (M . k))) +* (
j,
g)
in sum (N . k)
by A70, A75, GROUP_2:44;
for
j being
object st
j in J . k holds
(N . k) . j is
Subgroup of
M . k
by A73, GROUP_19:def 9;
then reconsider q =
((J . k) --> (1_ (M . k))) +* (
j,
g) as
finite-support Function of
(J . k),
(M . k) by A76, GROUP_19:10;
A77:
q =
(1_ (product (N . k))) +* (
j,
g)
by A74, GROUP_19:13
.=
(1_ (sum (N . k))) +* (
j,
g)
by GROUP_2:44
;
(N . k) . j is
Subgroup of
M . k
by A37, A38, A73, GROUP_19:def 9;
then
g is
Element of
(M . k)
by A39, GROUP_2:42;
then A78:
Product q = g
by A37, A38, GROUP_19:21;
hk . ((1_ (sum (N . k))) +* (j,g)) = g
by A45, A71, A77, A78;
then
(hk ") . (hk . ((1_ (product (N . k))) +* (j,g))) = (hk ") . g
by GROUP_2:44;
then A79:
(hk ") . g = (1_ (product (N . k))) +* (
j,
g)
by A45, A72, FUNCT_1:34;
per cases
( j <> n or j = n )
;
suppose A80:
j <> n
;
yi . n0 = xi . n0thus yi . n0 =
y . n
by A67, FUNCT_1:47
.=
1_ (UN . n1)
by A59, A80, GROUP_12:1
.=
1_ ((N . i) . n)
by Th19
.=
xi . n0
by A37, A38, A39, A65, A66, A79, A80, GROUP_12:1
;
verum end;
end; then
yi = xi
by A55, A57, GROUP_19:3;
hence
p . i0 = t . i0
by A43, Th25;
verum end;
end;
then A82:
z = (1ProdHom (M,k)) . g
by A49, A51, A53, FUNCT_1:2, GROUP_19:3;
g in M . k
by A41, GROUP_2:40;
then A83:
z = (1_ (product M)) +* (
k,
g)
by A82, GROUP_12:def 3;
z = (I --> (1_ G)) +* (
k,
g)
by A20, A83, GROUP_19:13;
hence
h . ((1ProdHom (UN,j)) . g) = g
by A28, A32, A36, GROUP_19:21;
verum
end;
hence
h . x = Product x
by A27, GROUP_20:18;
verum
end;
hence
Union N is internal DirectSumComponents of G, Union J
by A18, A26, GROUP_19:def 9; verum