let I be non empty set ; for G being Group
for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a
let G be Group; for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a
let F be Subgroup-Family of I,G; for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a
let h be Homomorphism of (sum F),G; for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a
let a be finite-support Function of I,G; ( a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) implies h . a = Product a )
assume that
A1:
a in sum F
and
A2:
for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x
; h . a = Product a
A3:
for i being object st i in I holds
F . i is Subgroup of G
by Def1;
defpred S1[ Nat] means for b being finite-support Function of I,G st b in sum F & card (support b) = $1 holds
h . b = Product b;
A4:
S1[ 0 ]
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
S1[k + 1]
let b be
finite-support Function of
I,
G;
( b in sum F & card (support b) = k + 1 implies h . b = Product b )
assume A8:
b in sum F
;
( not card (support b) = k + 1 or h . b = Product b )
assume A9:
card (support b) = k + 1
;
h . b = Product b
then
not
support b is
empty
;
then consider i being
object such that A10:
i in support b
by XBOOLE_0:def 1;
A11:
(
b . i <> 1_ G &
i in I )
by A10, GROUP_19:def 2;
reconsider i =
i as
Element of
I by A10;
set c =
b +* (
i,
(1_ (F . i)));
b +* (
i,
(1_ (F . i)))
in sum F
by A8, GROUP_19:25;
then reconsider c =
b +* (
i,
(1_ (F . i))) as
Element of
(sum F) ;
F . i is
Subgroup of
G
by Def1;
then A12:
1_ (F . i) = 1_ G
by GROUP_2:44;
then reconsider c0 =
c as
finite-support Function of
I,
G by GROUP_19:26;
A13:
b in product F
by A8, GROUP_2:40;
A14:
b . i in F . i
by A8, GROUP_19:5, GROUP_2:40;
then
(1ProdHom (F,i)) . (b . i) in ProjGroup (
F,
i)
by FUNCT_2:5;
then
(1ProdHom (F,i)) . (b . i) in sum F
by GROUP_2:40;
then reconsider d =
(1ProdHom (F,i)) . (b . i) as
Element of
(sum F) ;
A15:
d = (1_ (product F)) +* (
i,
(b . i))
by A14, GROUP_12:def 3;
A16:
d is
Element of
(product F)
by GROUP_2:42;
A17:
support (
d,
F)
= {i}
by A11, A12, A14, A15, A16, GROUP_19:18;
A18:
i in dom b
by A11, A13, GROUP_19:3;
A19:
b = c * d
proof
reconsider c1 =
c,
d1 =
d as
Element of
(product F) by GROUP_2:42;
A20:
support (
c1,
F)
misses support (
d1,
F)
A21:
dom (i .--> (b . i)) = {i}
;
A22:
dom (1_ (product F)) = I
by GROUP_19:3;
A23:
d1 | (support (d1,F)) =
((1_ (product F)) +* (i,(b . i))) | {i}
by A11, A12, A14, A15, GROUP_19:18
.=
((1_ (product F)) +* (i .--> (b . i))) | {i}
by A22, FUNCT_7:def 3
.=
i .--> (b . i)
by A21, FUNCT_4:23
;
A24:
i in dom c
by A18, FUNCT_7:30;
thus b =
c1 +* (
i,
(b . i))
by Th7
.=
c1 +* (d1 | (support (d1,F)))
by A23, A24, FUNCT_7:def 3
.=
c1 * d1
by A20, GROUP_19:31
.=
c * d
by GROUP_2:43
;
verum
end;
A25:
h . c0 = Product c0
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 that A27:
i <> j
and A28:
gi in F . i
and A29:
gj in F . j
;
gi * gj = gj * gi
set ai =
(1ProdHom (F,i)) . gi;
A30:
(1ProdHom (F,i)) . gi in ProjGroup (
F,
i)
by A28, FUNCT_2:5;
then
(1ProdHom (F,i)) . gi in sum F
by GROUP_2:40;
then reconsider ai =
(1ProdHom (F,i)) . gi as
Element of
(sum F) ;
reconsider bi =
ai as
Element of
(product F) by GROUP_2:42;
set aj =
(1ProdHom (F,j)) . gj;
A31:
(1ProdHom (F,j)) . gj in ProjGroup (
F,
j)
by A29, FUNCT_2:5;
then
(1ProdHom (F,j)) . gj in sum F
by GROUP_2:40;
then reconsider aj =
(1ProdHom (F,j)) . gj as
Element of
(sum F) ;
reconsider bj =
aj as
Element of
(product F) by GROUP_2:42;
A32:
gi = h . ai
by A2, A28;
gi * gj =
(h . ai) * (h . aj)
by A2, A29, A32
.=
h . (ai * aj)
by GROUP_6:def 6
.=
h . (bi * bj)
by GROUP_2:43
.=
h . (bj * bi)
by A27, A30, A31, GROUP_12:7
.=
h . (aj * ai)
by GROUP_2:43
.=
(h . aj) * (h . ai)
by GROUP_6:def 6
.=
gj * gi
by A2, A29, A32
;
hence
gi * gj = gj * gi
;
verum
end;
then A33:
F is
component-commutative
;
A34:
b in product F
by A8, GROUP_2:40;
h . b =
(h . c) * (h . d)
by A19, GROUP_6:def 6
.=
(Product c0) * (b . i)
by A2, A14, A25
.=
Product b
by A33, A34, Th8
;
hence
h . b = Product b
;
verum
end;
A35:
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A6);
consider k being Nat such that
A36:
card (support a) = k
;
thus
h . a = Product a
by A1, A35, A36; verum