let I be non empty set ; for G being Group
for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let G be Group; for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let a be finite-support Function of I,G; for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let W be finite Subset of I; ( support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) implies Product a = Product (a | W) )
assume that
A1:
support a c= W
and
A2:
for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i)
; Product a = Product (a | W)
reconsider ra = rng a as non empty Subset of G ;
for x, y being Element of G st x in ra & y in ra holds
x * y = y * x
then reconsider H = gr ra as non empty commutative Subgroup of G by Th44;
reconsider A = support a as finite Subset of W by A1;
reconsider B = W \ (support a) as finite Subset of W by XBOOLE_1:36;
per cases
( A = {} or A <> {} )
;
suppose A11:
A <> {}
;
Product a = Product (a | W)per cases
( B = {} or B <> {} )
;
suppose A12:
B <> {}
;
Product a = Product (a | W)
rng a c= [#] H
by GROUP_4:def 4;
then A14:
a is
Function of
I,
H
by FUNCT_2:6;
then reconsider fa =
a | (support a) as
A -defined the
carrier of
H -valued total Function ;
reconsider B0 =
B as
finite Subset of
I ;
reconsider fb =
a | B0 as
B0 -defined the
carrier of
H -valued total Function by A14;
A15:
A \/ B = W
by XBOOLE_1:45;
then reconsider fab =
a | W as
A \/ B -defined the
carrier of
H -valued total Function by A14;
A16:
A misses B
by XBOOLE_1:79;
A17:
dom fab =
A \/ B
by A15, FUNCT_2:def 1
.=
(dom fa) \/ B
by FUNCT_2:def 1
.=
(dom fa) \/ (dom fb)
by FUNCT_2:def 1
;
A18:
for
x being
object st
x in dom fab holds
fab . x = (fa +* fb) . x
A27:
dom (fa +* fb) = (dom fa) \/ (dom fb)
by FUNCT_4:def 1;
reconsider fca =
fa * (canFS A) as
FinSequence of
H by Th50;
reconsider fcsa =
fa * (canFS (support a)) as
FinSequence of
G by Th50;
reconsider fcab =
fab * (canFS (A \/ B)) as
FinSequence of
H by Th50;
reconsider fcw =
(a | W) * (canFS W) as
FinSequence of
G by Th50;
A31:
Product fa =
Product fca
by GROUP_17:def 1
.=
Product fcsa
by Th45
.=
Product a
by GROUP_17:def 1
;
A35:
fcab = fcw
by XBOOLE_1:45;
A36:
Product fab =
Product fcab
by GROUP_17:def 1
.=
Product fcw
by A35, Th45
.=
Product (a | W)
by GROUP_17:def 1
;
for
i being
object st
i in B0 holds
fb . i = 1_ H
then A41:
Product fb =
1_ H
by Th49
.=
1_ G
by GROUP_2:44
;
thus Product (a | W) =
(Product fa) * (Product fb)
by A11, A12, A16, A17, A18, A27, A36, FUNCT_1:2, GROUP_17:8
.=
(Product a) * (1_ G)
by A31, A41, GROUP_2:43
.=
Product a
by GROUP_1:def 4
;
verum end; end; end; end;