let I be non empty set ; for G being commutative 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 Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) ) )
let G be commutative 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 Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) ) )
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 Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) ) )
hereby ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) implies F is internal DirectSumComponents of G,I )
assume A1:
F is
internal DirectSumComponents of
G,
I
;
( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) )then A2:
( ( for
i being
Element of
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;
A3:
for
i being
object st
i in I holds
F . i is
Subgroup of
G
by A1, GROUP_19:54;
A4:
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 A5:
i <> j
;
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
A6:
F . i is
Subgroup of
G
by A1, GROUP_19:54;
then A7:
1_ G in F . i
by GROUP_2:46;
A8:
F . j is
Subgroup of
G
by A1, GROUP_19:54;
then
1_ G in F . j
by GROUP_2:46;
then
1_ G in ([#] (F . j)) /\ ([#] (F . i))
by A7, XBOOLE_0:def 4;
then A9:
{(1_ G)} c= ([#] (F . i)) /\ ([#] (F . j))
by ZFMISC_1:31;
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 A10:
x in ([#] (F . i)) /\ ([#] (F . j))
;
x in {(1_ G)}
reconsider gi =
x as
Element of
(F . i) by A10, XBOOLE_0:def 4;
reconsider gj =
x as
Element of
(F . j) by A10;
gi in G
by A6, GROUP_2:41;
then reconsider ggi =
gi as
Element of
G ;
gj in G
by A8, GROUP_2:41;
then reconsider ggj =
gj as
Element of
G ;
x = 1_ G
proof
assume A11:
x <> 1_ G
;
contradiction
set xi =
(1_ (product F)) +* (
i,
gi);
set xj =
(1_ (product F)) +* (
j,
gj);
A12:
(1_ (product F)) +* (
i,
gi)
in sum F
by GROUP_19:25, GROUP_2:46;
then reconsider xi =
(1_ (product F)) +* (
i,
gi) as
finite-support Function of
I,
G by A3, GROUP_19:10;
A13:
(1_ (product F)) +* (
j,
gj)
in sum F
by GROUP_19:25, GROUP_2:46;
then reconsider xj =
(1_ (product F)) +* (
j,
gj) as
finite-support Function of
I,
G by A3, GROUP_19:10;
A14:
1_ (product F) = I --> (1_ G)
by A2, GROUP_19:13;
then Product xi =
ggj
by GROUP_19:21
.=
Product xj
by A14, GROUP_19:21
;
then A15:
xi = xj
by A1, A12, A13, GROUP_19:54;
A16:
dom (1_ (product F)) = I
by GROUP_19:3;
xj . i =
(1_ (product F)) . i
by A5, FUNCT_7:32
.=
1_ (F . i)
by GROUP_7:6
.=
1_ G
by A6, GROUP_2:44
;
hence
contradiction
by A11, A15, A16, FUNCT_7:31;
verum
end;
hence
x in {(1_ G)}
by TARSKI:def 1;
verum
end;
then
([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)}
;
hence
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
by A9, XBOOLE_0:def 10;
verum
end; thus
( ( for
i being
Element of
I holds
F . i is
Subgroup of
G ) & ( for
i,
j being
Element of
I st
i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 A1, A4, GROUP_19:54;
verum
end;
assume A17:
( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 ) )
; F is internal DirectSumComponents of G,I
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
;
hence
F is internal DirectSumComponents of G,I
by A17, GROUP_19:54; verum