let G be Group; for I, J being non empty set
for F being internal DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is internal DirectSumComponents of G,I
let I, J be non empty set ; for F being internal DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is internal DirectSumComponents of G,I
let F be internal DirectSumComponents of G,J; for a being Function of I,J st a is bijective holds
F * a is internal DirectSumComponents of G,I
let a be Function of I,J; ( a is bijective implies F * a is internal DirectSumComponents of G,I )
assume A1:
a is bijective
; F * a is internal DirectSumComponents of G,I
then reconsider E = F * a as DirectSumComponents of G,I by Th13;
A2:
for i being Element of I holds E . i is Subgroup of G
A4:
for i being object st i in I holds
E . i is Subgroup of G
by A2;
ex h being Homomorphism of (sum E),G st
( h is bijective & ( for x being finite-support Function of I,G st x in sum E holds
h . x = Product x ) )
proof
consider hFG being
Homomorphism of
(sum F),
G such that A5:
hFG is
bijective
and A6:
for
y being
finite-support Function of
J,
G st
y in sum F holds
hFG . y = Product y
by GROUP_19:def 9;
reconsider hFE =
trans_sum (
F,
a) as
Homomorphism of
(sum F),
(sum E) by A1, TT;
A7:
hFE is
bijective
by A1, Th12;
then reconsider hEF =
hFE " as
Homomorphism of
(sum E),
(sum F) by GROUP_6:62;
reconsider h =
hFG * hEF as
Homomorphism of
(sum E),
G ;
take
h
;
( h is bijective & ( for x being finite-support Function of I,G st x in sum E holds
h . x = Product x ) )
A8:
hEF is
bijective
by A7, GROUP_6:63;
A9:
for
i being
Element of
I for
g being
Element of
(E . i) holds
h . ((1ProdHom (E,i)) . g) = g
proof
let i be
Element of
I;
for g being Element of (E . i) holds h . ((1ProdHom (E,i)) . g) = glet g be
Element of
(E . i);
h . ((1ProdHom (E,i)) . g) = g
(1_ (product E)) +* (
i,
g)
in sum E
by GROUP_19:25, GROUP_2:46;
then reconsider x =
(1_ (product E)) +* (
i,
g) as
Element of
(sum E) ;
reconsider j =
a . i as
Element of
J ;
A10:
dom a = I
by FUNCT_2:def 1;
then A11:
E . i = F . j
by FUNCT_1:13;
reconsider g1 =
g as
Element of
(F . j) by A10, FUNCT_1:13;
F . j is
Subgroup of
G
by A2, A11;
then
[#] (F . j) c= [#] G
by GROUP_2:def 5;
then reconsider g2 =
g1 as
Element of
G ;
reconsider y =
hEF . x as
Element of
(sum F) ;
A12:
for
j being
object st
j in J holds
F . j is
Subgroup of
G
by GROUP_19:def 9;
y in sum F
;
then reconsider y1 =
y as
finite-support Function of
J,
G by A12, GROUP_19:10;
A13:
hFE = (trans_prod (F,a)) | (sum F)
by A1, Def3;
A14:
x = y * a
A17:
y = (J --> (1_ G)) +* (
j,
g2)
proof
reconsider z =
(J --> (1_ G)) +* (
j,
g2) as
Function ;
y is
Element of
(product F)
by GROUP_2:42;
then A18:
dom y = J
by GROUP_19:3;
A19:
dom (J --> (1_ G)) = J
by FUNCOP_1:13;
for
j0 being
object st
j0 in J holds
y . j0 = z . j0
proof
let j0 be
object ;
( j0 in J implies y . j0 = z . j0 )
assume
j0 in J
;
y . j0 = z . j0
then reconsider j0 =
j0 as
Element of
J ;
A20:
dom (1_ (product E)) = I
by GROUP_19:3;
per cases
( j0 = j or j0 <> j )
;
suppose A22:
j0 <> j
;
y . j0 = z . j0A23:
(
a is
one-to-one &
rng a = J )
by A1, FUNCT_2:def 3;
then reconsider ia =
a " as
Function of
J,
I by FUNCT_2:25;
reconsider i0 =
ia . j0 as
Element of
I ;
A24:
ia . j =
(ia * a) . i
by A10, FUNCT_1:13
.=
(id I) . i
by A23, FUNCT_2:29
.=
i
;
A25:
dom ia = J
by FUNCT_2:def 1;
A26:
ia is
one-to-one
by A1;
A27:
j0 =
(id J) . j0
.=
(a * ia) . j0
by A23, FUNCT_2:29
.=
a . i0
by A25, FUNCT_1:13
;
A28:
y . j0 =
(y * a) . i0
by A10, A27, FUNCT_1:13
.=
(1_ (product E)) . i0
by A14, A22, A24, A25, A26, FUNCT_7:32
.=
(I --> (1_ G)) . i0
by A2, GROUP_19:13
.=
1_ G
by FUNCOP_1:7
;
z . j0 =
(J --> (1_ G)) . j0
by A22, FUNCT_7:32
.=
1_ G
by FUNCOP_1:7
;
hence
y . j0 = z . j0
by A28;
verum end;
end;
hence
y = (J --> (1_ G)) +* (
j,
g2)
by A18, A19, FUNCT_7:30;
verum
end;
y in sum F
;
then A29:
hFG . y =
Product y1
by A6
.=
g2
by A17, GROUP_19:21
;
x in sum E
;
then A30:
x in dom hEF
by FUNCT_2:def 1;
h . x = g
by A29, A30, FUNCT_1:13;
hence
h . ((1ProdHom (E,i)) . g) = g
by GROUP_12:def 3;
verum
end;
E is
Subgroup-Family of
I,
G
by A4, GROUP_20:def 1;
hence
(
h is
bijective & ( for
x being
finite-support Function of
I,
G st
x in sum E holds
h . x = Product x ) )
by A5, A8, A9, GROUP_20:18, GROUP_6:64;
verum
end;
hence
F * a is internal DirectSumComponents of G,I
by A2, GROUP_19:def 9; verum