let I be non empty set ; for G being strict Group
for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )
let G be strict Group; for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )
let F be Group-Family of I; ( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )
A1:
dom F = I
by PARTFUN1:def 2;
A2:
dom (Carrier F) = I
by PARTFUN1:def 2;
hereby ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) implies F is internal DirectSumComponents of G,I )
assume A3:
F is
internal DirectSumComponents of
G,
I
;
( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) )then A4:
( ( for
i being
object st
i in I holds
F . i is
Subgroup of
G ) & ( for
i,
j being
Element of
I for
gi,
gj being
Element of
G st
i <> j &
gi in F . i &
gj in F . j holds
gi * gj = gj * gi ) & ( for
y being
Element of
G ex
x being
finite-support Function of
I,
G st
(
x in sum F &
y = Product x ) ) & ( for
x1,
x2 being
finite-support Function of
I,
G st
x1 in sum F &
x2 in sum F &
Product x1 = Product x2 holds
x1 = x2 ) )
by GROUP_19:54;
then A5:
F is
component-commutative Subgroup-Family of
I,
G
by Def1, Def2;
for
x being
object st
x in Union (Carrier F) holds
x in [#] G
then
Union (Carrier F) c= [#] G
;
then reconsider UF =
Union (Carrier F) as
Subset of
G ;
A9:
for
g being
Element of
G holds
g in gr UF
then A12:
gr UF = G
by GROUP_2:62;
thus
for
i being
Element of
I holds
F . i is
normal Subgroup of
G
by A5, A12, Th14;
( ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) )thus
ex
UF being
Subset of
G st
(
UF = Union (Carrier F) &
gr UF = G )
by A9, GROUP_2:62;
for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )thus
for
i being
Element of
I ex
UFi being
Subset of
G st
(
UFi = Union ((Carrier F) | (I \ {i})) &
([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )
verumproof
let i be
Element of
I;
ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )
A13:
for
i being
Element of
I holds
F . i is
Subgroup of
G
by A3, GROUP_19:54;
per cases
( I \ {i} = {} or I \ {i} <> {} )
;
suppose A16:
I \ {i} <> {}
;
ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )set CFi =
(Carrier F) | (I \ {i});
set UFi =
Union ((Carrier F) | (I \ {i}));
for
x being
object st
x in Union ((Carrier F) | (I \ {i})) holds
x in [#] G
then reconsider UFi =
Union ((Carrier F) | (I \ {i})) as
Subset of
G by TARSKI:def 3;
take
UFi
;
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )thus
UFi = Union ((Carrier F) | (I \ {i}))
;
([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)}A21:
1_ G in gr UFi
by GROUP_2:46;
F . i is
Subgroup of
G
by A3, GROUP_19:54;
then
1_ G in F . i
by GROUP_2:46;
then
1_ G in ([#] (gr UFi)) /\ ([#] (F . i))
by A21, XBOOLE_0:def 4;
then A22:
{(1_ G)} c= ([#] (gr UFi)) /\ ([#] (F . i))
by ZFMISC_1:31;
for
x being
object st
x in ([#] (gr UFi)) /\ ([#] (F . i)) holds
x in {(1_ G)}
proof
let x be
object ;
( x in ([#] (gr UFi)) /\ ([#] (F . i)) implies x in {(1_ G)} )
assume A23:
x in ([#] (gr UFi)) /\ ([#] (F . i))
;
x in {(1_ G)}
then
(
x in [#] (gr UFi) &
x in [#] (F . i) )
by XBOOLE_0:def 4;
then reconsider g =
x as
Element of
G by GROUP_2:def 5, TARSKI:def 3;
set I0 =
I \ {i};
set F0 =
F | (I \ {i});
A24:
dom (F | (I \ {i})) = I \ {i}
by A1, RELAT_1:62;
A25:
for
j being
object st
j in I \ {i} holds
(F | (I \ {i})) . j is
Subgroup of
G
then
for
j being
object st
j in I \ {i} holds
(F | (I \ {i})) . j is
Group
;
then reconsider F0 =
F | (I \ {i}) as
Group-Family of
I \ {i} by A24, GROUP_19:2;
reconsider F0 =
F0 as
Subgroup-Family of
I \ {i},
G by A25, Def1;
A29:
F0 is
component-commutative
proof
let j,
k be
object ;
GROUP_20:def 2 for gi, gj being Element of G st j in I \ {i} & k in I \ {i} & j <> k holds
ex Fi, Fj being Subgroup of G st
( Fi = F0 . j & Fj = F0 . k & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )let gj,
gk be
Element of
G;
( j in I \ {i} & k in I \ {i} & j <> k implies ex Fi, Fj being Subgroup of G st
( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) ) )
assume A28:
(
j in I \ {i} &
k in I \ {i} &
j <> k )
;
ex Fi, Fj being Subgroup of G st
( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) )
then reconsider Fj =
F0 . j,
Fk =
F0 . k as
Subgroup of
G by Def1;
take
Fj
;
ex Fj being Subgroup of G st
( Fj = F0 . j & Fj = F0 . k & ( gj in Fj & gk in Fj implies gj * gk = gk * gj ) )
take
Fk
;
( Fj = F0 . j & Fk = F0 . k & ( gj in Fj & gk in Fk implies gj * gk = gk * gj ) )
thus
(
Fj = F0 . j &
Fk = F0 . k )
;
( gj in Fj & gk in Fk implies gj * gk = gk * gj )
assume A29:
(
gj in Fj &
gk in Fk )
;
gj * gk = gk * gj
reconsider j =
j,
k =
k as
Element of
I by A28;
(
F0 . j = F . j &
F0 . k = F . k )
by A28, FUNCT_1:49;
hence
gj * gk = gk * gj
by A3, A28, A29, GROUP_19:54;
verum
end;
A30:
dom (Carrier F0) = I \ {i}
by PARTFUN1:def 2;
for
j being
object st
j in dom ((Carrier F) | (I \ {i})) holds
((Carrier F) | (I \ {i})) . j = (Carrier F0) . j
then A33:
UFi = Union (Carrier F0)
by A2, A30, FUNCT_1:2, RELAT_1:62;
g in gr UFi
by A23, XBOOLE_0:def 4;
then consider hi being
finite-support Function of
(I \ {i}),
(gr UFi) such that A34:
(
hi in sum F0 &
g = Product hi )
by A16, A29, A33, Th13;
set h =
hi +* ({i} --> (1_ G));
A35:
rng (hi +* ({i} --> (1_ G))) c= (rng hi) \/ (rng ({i} --> (1_ G)))
by FUNCT_4:17;
rng hi c= [#] G
by GROUP_2:def 5, TARSKI:def 3;
then
(rng hi) \/ (rng ({i} --> (1_ G))) c= [#] G
by XBOOLE_1:8;
then A36:
rng (hi +* ({i} --> (1_ G))) c= [#] G
by A35;
A37:
dom ({i} --> (1_ G)) = {i}
;
dom hi = I \ {i}
by FUNCT_2:def 1;
then A38:
dom (hi +* ({i} --> (1_ G))) =
(I \ {i}) \/ {i}
by A37, FUNCT_4:def 1
.=
I
by XBOOLE_1:45
;
then reconsider h =
hi +* ({i} --> (1_ G)) as
Function of
I,
G by A36, FUNCT_2:2;
A39:
for
j being
object holds
(
j in support h iff
j in support hi )
then A49:
support h = support hi
by TARSKI:2;
then reconsider h =
h as
finite-support Function of
I,
G by GROUP_19:def 3;
A50:
support h = dom (h | (support h))
by PARTFUN1:def 2;
A51:
support hi = dom (hi | (support hi))
by PARTFUN1:def 2;
for
x being
object st
x in dom (h | (support h)) holds
(h | (support h)) . x = (hi | (support hi)) . x
then A55:
h | (support h) = hi | (support hi)
by A39, A50, A51, FUNCT_1:2, TARSKI:2;
reconsider fh =
(h | (support h)) * (canFS (support h)) as
FinSequence of
G by FINSEQ_2:32;
reconsider fhi =
(hi | (support hi)) * (canFS (support hi)) as
FinSequence of
(gr UFi) by FINSEQ_2:32;
A56:
g =
Product fhi
by A34, GROUP_17:def 1
.=
Product fh
by A49, A55, GROUP_19:45
.=
Product h
by GROUP_17:def 1
;
A57:
i in {i}
by TARSKI:def 1;
A58:
dom ({i} --> (1_ G)) = {i}
;
A59:
h in product F
A65:
h in sum F
reconsider id1g =
I --> (1_ G) as
Function of
I,
G ;
support id1g is
empty
by GROUP_19:12;
then reconsider id1g =
id1g as
finite-support Function of
I,
G by GROUP_19:def 3;
A66:
1_ (product F) = id1g
by A13, GROUP_19:13;
then reconsider k =
(1_ (product F)) +* (
i,
g) as
finite-support Function of
I,
G by GROUP_19:26;
A67:
Product k = g
by A66, GROUP_19:21;
k in ProjSet (
F,
i)
by A23, GROUP_12:def 1;
then
k in ProjGroup (
F,
i)
by GROUP_12:def 2;
then A68:
k in sum F
by GROUP_2:40;
dom (1_ (product F)) = I
by GROUP_19:3;
then g =
k . i
by FUNCT_7:31
.=
h . i
by A3, A56, A65, A67, A68, GROUP_19:54
.=
({i} --> (1_ G)) . i
by A57, A58, FUNCT_4:13
.=
1_ G
by A57, FUNCOP_1:7
;
hence
x in {(1_ G)}
by TARSKI:def 1;
verum
end; then
([#] (gr UFi)) /\ ([#] (F . i)) c= {(1_ G)}
;
hence
([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)}
by A22, XBOOLE_0:def 10;
verum end; end;
end;
end;
assume that
A69:
for i being Element of I holds F . i is normal Subgroup of G
and
A70:
ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G )
and
A71:
for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )
; F is internal DirectSumComponents of G,I
consider UF being Subset of G such that
A72:
( UF = Union (Carrier F) & gr UF = G )
by A70;
A73:
for i being Element of I holds F . i is Subgroup of G
by A69;
A74:
for i being object st i in I holds
F . i is Subgroup of G
by A69;
A75:
for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
proof
let i,
j be
Element of
I;
( i <> j implies ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} )
assume A76:
i <> j
;
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
F . i is
Subgroup of
G
by A69;
then
1_ G in F . i
by GROUP_2:46;
then A77:
{(1_ G)} c= [#] (F . i)
by ZFMISC_1:31;
F . j is
Subgroup of
G
by A69;
then
1_ G in F . j
by GROUP_2:46;
then
{(1_ G)} c= [#] (F . j)
by ZFMISC_1:31;
then A78:
{(1_ G)} c= ([#] (F . i)) /\ ([#] (F . j))
by A77, XBOOLE_1:19;
for
x being
object st
x in ([#] (F . i)) /\ ([#] (F . j)) holds
x in {(1_ G)}
proof
let x be
object ;
( x in ([#] (F . i)) /\ ([#] (F . j)) implies x in {(1_ G)} )
assume A79:
x in ([#] (F . i)) /\ ([#] (F . j))
;
x in {(1_ G)}
then A80:
(
x in [#] (F . i) &
x in [#] (F . j) )
by XBOOLE_0:def 4;
consider UFj being
Subset of
G such that A81:
(
UFj = Union ((Carrier F) | (I \ {j})) &
([#] (gr UFj)) /\ ([#] (F . j)) = {(1_ G)} )
by A71;
(
i in I & not
i in {j} )
by A76, TARSKI:def 1;
then A82:
i in I \ {j}
by XBOOLE_0:def 5;
A83:
i in dom ((Carrier F) | (I \ {j}))
by A2, A82, RELAT_1:62;
((Carrier F) | (I \ {j})) . i =
(Carrier F) . i
by A82, FUNCT_1:49
.=
[#] (F . i)
by PENCIL_3:7
;
then
[#] (F . i) c= union (rng ((Carrier F) | (I \ {j})))
by A83, FUNCT_1:3, ZFMISC_1:74;
then A84:
[#] (F . i) c= UFj
by A81, CARD_3:def 4;
UFj c= [#] (gr UFj)
by GROUP_4:def 4;
then
x in [#] (gr UFj)
by A80, A84;
hence
x in {(1_ G)}
by A79, A81, XBOOLE_0:def 4;
verum
end;
then
([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)}
;
hence
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
by A78, XBOOLE_0:def 10;
verum
end;
A85:
for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
proof
let i,
j be
Element of
I;
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gilet gi,
gj be
Element of
G;
( i <> j & gi in F . i & gj in F . j implies gi * gj = gj * gi )
assume A86:
(
i <> j &
gi in F . i &
gj in F . j )
;
gi * gj = gj * gi
A87:
F . i is
normal Subgroup of
G
by A69;
A88:
F . j is
normal Subgroup of
G
by A69;
A89:
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
by A75, A86;
set x =
(gi * gj) * ((gj * gi) ");
A90:
gi " in F . i
by A86, A87, GROUP_2:51;
A91:
gj " in F . j
by A86, A88, GROUP_2:51;
A92:
(gi * gj) * (gi ") in F . j
by A86, A88, Th1;
A93:
gj * ((gi ") * (gj ")) in F . i
by A87, A90, Th1;
(gi * gj) * ((gj * gi) ") =
(gi * gj) * ((gi ") * (gj "))
by GROUP_1:17
.=
((gi * gj) * (gi ")) * (gj ")
by GROUP_1:def 3
;
then A94:
(gi * gj) * ((gj * gi) ") in F . j
by A88, A91, A92, GROUP_2:50;
(gi * gj) * ((gj * gi) ") =
(gi * gj) * ((gi ") * (gj "))
by GROUP_1:17
.=
gi * (gj * ((gi ") * (gj ")))
by GROUP_1:def 3
;
then
(gi * gj) * ((gj * gi) ") in F . i
by A86, A87, A93, GROUP_2:50;
then
(gi * gj) * ((gj * gi) ") in ([#] (F . i)) /\ ([#] (F . j))
by A94, XBOOLE_0:def 4;
then
(gi * gj) * ((gj * gi) ") = 1_ G
by A89, TARSKI:def 1;
then
(gi * gj) " = (gj * gi) "
by GROUP_1:12;
hence
gi * gj = gj * gi
by GROUP_1:9;
verum
end;
A95:
F is component-commutative Subgroup-Family of I,G
by A74, A85, Def1, Def2;
A96:
for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x )
for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2
by A71, A95, Th15;
hence
F is internal DirectSumComponents of G,I
by A73, A85, A96, GROUP_19:54; verum