let G be Group; for I1, I2 being non empty set
for F1 being internal DirectSumComponents of G,I1
for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
let I1, I2 be non empty set ; for F1 being internal DirectSumComponents of G,I1
for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
let F1 be internal DirectSumComponents of G,I1; for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
let F2 be Subgroup-Family of I2,G; ( I1 misses I2 & F2 = I2 --> ((1). G) implies F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2 )
assume that
A1:
I1 misses I2
and
A2:
F2 = I2 --> ((1). G)
; F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
reconsider I = {1,2} as non empty set ;
set J = {[1,I1],[2,I2]};
for x, y1, y2 being object st [x,y1] in {[1,I1],[2,I2]} & [x,y2] in {[1,I1],[2,I2]} holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in {[1,I1],[2,I2]} & [x,y2] in {[1,I1],[2,I2]} implies y1 = y2 )
assume
(
[x,y1] in {[1,I1],[2,I2]} &
[x,y2] in {[1,I1],[2,I2]} )
;
y1 = y2
then A3:
( (
[x,y1] = [1,I1] or
[x,y1] = [2,I2] ) & (
[x,y2] = [1,I1] or
[x,y2] = [2,I2] ) )
by TARSKI:def 2;
end;
then reconsider J = {[1,I1],[2,I2]} as Function by FUNCT_1:def 1;
dom J = I
by RELAT_1:10;
then reconsider J = J as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A4:
rng J = {I1,I2}
by RELAT_1:10;
( [1,I1] in J & [2,I2] in J )
by TARSKI:def 2;
then A5:
( 1 in dom J & J . 1 = I1 & 2 in dom J & J . 2 = I2 )
by FUNCT_1:1;
not {} in rng J
then
J is non-empty
;
then reconsider J = J as non-empty ManySortedSet of I ;
for i, j being object st i <> j holds
J . i misses J . j
then
J is disjoint_valued
;
then reconsider J = J as non-empty disjoint_valued ManySortedSet of I ;
reconsider M = <*G,((1). G)*> as Group-Family of I ;
A8:
for x, y being Function st x in [#] (product M) & y in [#] (product M) & x . 1 = y . 1 holds
x = y
set h1 = id the carrier of G;
for a, b being Element of G holds (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b)
;
then reconsider h1 = id the carrier of G as Homomorphism of G,G by GROUP_6:def 6;
set CS1 = the carrier of (product M);
set CS2 = the carrier of G;
defpred S1[ Element of the carrier of (product M), Element of the carrier of G] means $2 = h1 . ($1 . 1);
A15:
for x being Element of the carrier of (product M) ex y being Element of the carrier of G st S1[x,y]
consider h being Function of the carrier of (product M), the carrier of G such that
A17:
for x being Element of the carrier of (product M) holds S1[x,h . x]
from FUNCT_2:sch 3(A15);
reconsider h = h as Function of the carrier of (product M), the carrier of G ;
A18:
for x1, x2 being object st x1 in the carrier of (product M) & x2 in the carrier of (product M) & h . x1 = h . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in the carrier of (product M) & x2 in the carrier of (product M) & h . x1 = h . x2 implies x1 = x2 )
assume A19:
(
x1 in the
carrier of
(product M) &
x2 in the
carrier of
(product M) &
h . x1 = h . x2 )
;
x1 = x2
then reconsider x10 =
x1,
x20 =
x2 as
Element of the
carrier of
(product M) ;
A20:
(
h . x10 = h1 . (x10 . 1) &
h . x20 = h1 . (x20 . 1) )
by A17;
A21:
x1 in product M
by A19;
reconsider z1 =
x1 as
Function by A19;
B6:
1 is
Element of
I
by TARSKI:def 2;
then reconsider M1 =
M . 1 as
Group by GROUP_19:1;
z1 . 1
in M1
by A21, B6, GROUP_19:5;
then A22:
x10 . 1
in the
carrier of
G
by FINSEQ_1:44;
A23:
x2 in product M
by A19;
reconsider z2 =
x2 as
Function by A19;
z2 . 1
in M1
by A23, B6, GROUP_19:5;
then A24:
x20 . 1
in the
carrier of
G
by FINSEQ_1:44;
x10 . 1
= x20 . 1
by A19, A20, A22, A24, FUNCT_2:19;
hence
x1 = x2
by A8;
verum
end;
then A25:
h is one-to-one
by FUNCT_2:19;
for y being object st y in the carrier of G holds
ex x being object st
( x in the carrier of (product M) & y = h . x )
then
rng h = the carrier of G
by FUNCT_2:10;
then A27:
h is onto
by FUNCT_2:def 3;
A28:
for a, b being Element of the carrier of (product M) holds h . (a * b) = (h . a) * (h . b)
product M = sum M
by GROUP_7:9;
then A33:
h is Homomorphism of (sum M),G
by A28, GROUP_6:def 6;
then reconsider M = <*G,((1). G)*> as DirectSumComponents of G,I by A25, A27, GROUP_19:def 8;
A34:
for i being Element of I holds M . i is Subgroup of G
for x being finite-support Function of I,G st x in sum M holds
h . x = Product x
then reconsider M = M as internal DirectSumComponents of G,I by A25, A27, A33, A34, GROUP_19:def 9;
set N = <*F1,F2*>;
len <*F1,F2*> = 2
by FINSEQ_1:44;
then
dom <*F1,F2*> = I
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider N = <*F1,F2*> as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A39:
for i being Element of I holds N . i is Group-Family of J . i
then
for i being Element of I holds N . i is multMagma-Family of J . i
;
then reconsider N = N as multMagma-Family of I,J by Def4;
reconsider N = N as Group-Family of I,J by A39, Def5;
A40:
for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i
proof
let i be
Element of
I;
N . i is internal DirectSumComponents of M . i,J . i
per cases
( i = 1 or i = 2 )
by TARSKI:def 2;
suppose A42:
i = 2
;
N . i is internal DirectSumComponents of M . i,J . i
for
i being
Element of
I2 holds
card (F2 . i) = 1
then A43:
card the
carrier of
(sum F2) = 1
by Th43;
card {0} = 1
by CARD_1:30;
then consider a being
object such that A44:
the
carrier of
(sum F2) = {a}
by A43, CARD_1:29;
A45:
the
carrier of
(sum F2) = {(1_ (sum F2))}
by A44, TARSKI:def 1;
reconsider Z = the
carrier of
(sum F2) as non
empty set ;
set h =
Z --> (1_ G);
A46:
(
dom (Z --> (1_ G)) = the
carrier of
(sum F2) &
rng (Z --> (1_ G)) c= {(1_ G)} )
by FUNCOP_1:13;
{(1_ G)} = the
carrier of
((1). G)
by GROUP_2:def 7;
then reconsider h =
Z --> (1_ G) as
Function of the
carrier of
(sum F2), the
carrier of
((1). G) by A46, FUNCT_2:2;
for
a,
b being
Element of the
carrier of
(sum F2) holds
h . (a * b) = (h . a) * (h . b)
then reconsider h =
h as
Homomorphism of
(sum F2),
((1). G) by GROUP_6:def 6;
for
x1,
x2 being
object st
x1 in the
carrier of
(sum F2) &
x2 in the
carrier of
(sum F2) &
h . x1 = h . x2 holds
x1 = x2
then A49:
h is
one-to-one
by FUNCT_2:19;
for
y being
object st
y in the
carrier of
((1). G) holds
ex
x being
object st
(
x in the
carrier of
(sum F2) &
y = h . x )
then
rng h = the
carrier of
((1). G)
by FUNCT_2:10;
then A51:
h is
onto
by FUNCT_2:def 3;
A52:
(
N . i = F2 &
M . i = (1). G )
by A42, FINSEQ_1:44;
then reconsider h =
h as
Homomorphism of
(sum (N . i)),
(M . i) by A5, A42;
reconsider Ni =
N . i as
DirectSumComponents of
M . i,
J . i by A5, A42, A49, A51, A52, GROUP_19:def 8;
A53:
for
j being
Element of
J . i holds
Ni . j is
Subgroup of
M . i
A54:
for
x being
finite-support Function of
(J . i),
(M . i) st
x in sum Ni holds
h . x = Product x
proof
let x be
finite-support Function of
(J . i),
(M . i);
( x in sum Ni implies h . x = Product x )
assume A55:
x in sum Ni
;
h . x = Product x
for
k being
object st
k in J . i holds
x . k = 1_ (M . i)
proof
let k be
object ;
( k in J . i implies x . k = 1_ (M . i) )
assume A56:
k in J . i
;
x . k = 1_ (M . i)
then reconsider k0 =
k as
Element of
J . i ;
reconsider N =
F2 . k0 as
1-sorted by A2, A5, A42, FUNCOP_1:7;
A57:
F2 . k = (1). G
by A2, A5, A42, A56, FUNCOP_1:7;
x in sum F2
by A5, A42, A55, FINSEQ_1:44;
then
x . k0 in N
by A5, A42, GROUP_2:40, GROUP_19:5;
then A58:
x . k in {(1_ G)}
by A57, GROUP_2:def 7;
1_ G =
1_ ((1). G)
by GROUP_2:44
.=
1_ (M . i)
by A42, FINSEQ_1:44
;
hence
x . k = 1_ (M . i)
by A58, TARSKI:def 1;
verum
end;
then Product x =
1_ (M . i)
by Th44
.=
1_ ((1). G)
by A42, FINSEQ_1:44
.=
1_ G
by GROUP_2:44
;
hence
h . x = Product x
by A5, A42, A52, A55, FUNCOP_1:7;
verum
end;
Ni is
internal
by A49, A51, A52, A53, A54;
hence
N . i is
internal DirectSumComponents of
M . i,
J . i
;
verum
end;
A59:
I1 \/ I2 = Union J
by A4, ZFMISC_1:75;
A60: dom (Union N) =
Union J
by PARTFUN1:def 2
.=
(dom F1) \/ I2
by A59, PARTFUN1:def 2
.=
(dom F1) \/ (dom F2)
by PARTFUN1:def 2
;
for x being object st x in (dom F1) \/ (dom F2) holds
( ( x in dom F2 implies (Union N) . x = F2 . x ) & ( not x in dom F2 implies (Union N) . x = F1 . x ) )
then
F1 +* F2 = Union N
by A60, FUNCT_4:def 1;
hence
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
by A40, A59, Th40; verum