P. 184 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18301-18400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	giccyg 18301	Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( G ~=g𝑔 H -> ( G e. CycGrp -> H e. CycGrp ) )
Theorem	cycsubgcyg 18302*	The cyclic subgroup generated by A is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- S = ran ( x e. ZZ |-> ( x .x. A ) )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( G ↾s S ) e. CycGrp )
Theorem	cycsubgcyg2 18303	The cyclic subgroup generated by A is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- B = ( Base ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( G e. Grp /\ A e. B ) -> ( G ↾s ( K ` { A } ) ) e. CycGrp )
10.3.3  Group sum operation
Theorem	gsumval3a 18304*	Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by AV, 29-May-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> W e. Fin )   &    |- ( ph -> W =/= (/) )   &    |- W = ( F supp .0. )   &    |- ( ph -> -. A e. ran ... )   =>    |- ( ph -> ( G gsumg F ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
Theorem	gsumval3eu 18305*	The group sum as defined in gsumval3a 18304 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> W e. Fin )   &    |- ( ph -> W =/= (/) )   &    |- ( ph -> W C_ A )   =>    |- ( ph -> E! x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )
Theorem	gsumval3lem1 18306*	Lemma 1 for gsumval3 18308. (Contributed by AV, 31-May-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> H : ( 1 ... M ) -1-1-> A )   &    |- ( ph -> ( F supp .0. ) C_ ran H )   &    |- W = ( ( F o. H ) supp .0. )   =>    |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) )
Theorem	gsumval3lem2 18307*	Lemma 2 for gsumval3 18308. (Contributed by AV, 31-May-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> H : ( 1 ... M ) -1-1-> A )   &    |- ( ph -> ( F supp .0. ) C_ ran H )   &    |- W = ( ( F o. H ) supp .0. )   =>    |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )
Theorem	gsumval3 18308	Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> H : ( 1 ... M ) -1-1-> A )   &    |- ( ph -> ( F supp .0. ) C_ ran H )   &    |- W = ( ( F o. H ) supp .0. )   =>    |- ( ph -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
Theorem	gsumcllem 18309*	Lemma for gsumcl 18316 and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.)
|- ( ph -> F : A --> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> Z e. U )   &    |- ( ph -> ( F supp Z ) C_ W )   =>    |- ( ( ph /\ W = (/) ) -> F = ( k e. A |-> Z ) )
Theorem	gsumzres 18310	Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> ( F supp .0. ) C_ W )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( F |` W ) ) = ( G gsumg F ) )
Theorem	gsumzcl2 18311	Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 18312, because it is not required that F is a function (actually, the hypothesis always holds for any proper class F). (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> ( F supp .0. ) e. Fin )   =>    |- ( ph -> ( G gsumg F ) e. B )
Theorem	gsumzcl 18312	Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) e. B )
Theorem	gsumzf1o 18313	Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 2-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H : C -1-1-onto-> A )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
Theorem	gsumres 18314	Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ( F supp .0. ) C_ W )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( F |` W ) ) = ( G gsumg F ) )
Theorem	gsumcl2 18315	Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 18316, because it is not required that F is a function (actually, the hypothesis always holds for any proper class F). (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ( F supp .0. ) e. Fin )   =>    |- ( ph -> ( G gsumg F ) e. B )
Theorem	gsumcl 18316	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) e. B )
Theorem	gsumf1o 18317	Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H : C -1-1-onto-> A )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
Theorem	gsumzsubmcl 18318	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) e. S )
Theorem	gsumsubmcl 18319	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) e. S )
Theorem	gsumsubgcl 18320	Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.)
|- .0. = ( 0g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. V )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) e. S )
Theorem	gsumzaddlem 18321*	The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   &    |- W = ( ( F u. H ) supp .0. )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> H : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> ran H C_ ( Z ` ran H ) )   &    |- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )   &    |- ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumzadd 18322	The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> S C_ ( Z ` S ) )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> H : A --> S )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumadd 18323	The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> H : A --> B )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsummptfsadd 18324*	The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 9-Jul-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- ( ph -> F = ( x e. A |-> C ) )   &    |- ( ph -> H = ( x e. A |-> D ) )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   =>    |- ( ph -> ( G gsumg ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsummptfidmadd 18325*	The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- F = ( x e. A |-> C )   &    |- H = ( x e. A |-> D )   =>    |- ( ph -> ( G gsumg ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsummptfidmadd2 18326*	The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- F = ( x e. A |-> C )   &    |- H = ( x e. A |-> D )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumzsplit 18327	Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` C ) ) .+ ( G gsumg ( F |` D ) ) ) )
Theorem	gsumsplit 18328	Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` C ) ) .+ ( G gsumg ( F |` D ) ) ) )
Theorem	gsumsplit2 18329*	Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   =>    |- ( ph -> ( G gsumg ( k e. A |-> X ) ) = ( ( G gsumg ( k e. C |-> X ) ) .+ ( G gsumg ( k e. D |-> X ) ) ) )
Theorem	gsummptfidmsplit 18330*	Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> Y e. B )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   =>    |- ( ph -> ( G gsumg ( k e. A |-> Y ) ) = ( ( G gsumg ( k e. C |-> Y ) ) .+ ( G gsumg ( k e. D |-> Y ) ) ) )
Theorem	gsummptfidmsplitres 18331*	Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> Y e. B )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   &    |- F = ( k e. A |-> Y )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` C ) ) .+ ( G gsumg ( F |` D ) ) ) )
Theorem	gsummptfzsplit 18332*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by AV, 25-Oct-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> Y e. B )   =>    |- ( ph -> ( G gsumg ( k e. ( 0 ... ( N + 1 ) ) |-> Y ) ) = ( ( G gsumg ( k e. ( 0 ... N ) |-> Y ) ) .+ ( G gsumg ( k e. { ( N + 1 ) } |-> Y ) ) ) )
Theorem	gsummptfzsplitl 18333*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, , extracting a singleton from the left. (Contributed by AV, 7-Nov-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> Y e. B )   =>    |- ( ph -> ( G gsumg ( k e. ( 0 ... N ) |-> Y ) ) = ( ( G gsumg ( k e. ( 1 ... N ) |-> Y ) ) .+ ( G gsumg ( k e. { 0 } |-> Y ) ) ) )
Theorem	gsumconst 18334*	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsumg ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
Theorem	gsumconstf 18335*	Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.)
|- F/_ k X   &    |- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsumg ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
Theorem	gsummptshft 18336*	Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. B )   &    |- ( j = ( k - K ) -> A = C )   =>    |- ( ph -> ( G gsumg ( j e. ( M ... N ) |-> A ) ) = ( G gsumg ( k e. ( ( M + K ) ... ( N + K ) ) |-> C ) ) )
Theorem	gsumzmhm 18337	Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
Theorem	gsummhm 18338	Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
Theorem	gsummhm2 18339*	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gsumg ( k e. A |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gsumg ( k e. A |-> D ) ) = E )
Theorem	gsummptmhm 18340*	Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018.) (Revised by AV, 8-Sep-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ph -> ( x e. A |-> C ) finSupp .0. )   =>    |- ( ph -> ( H gsumg ( x e. A |-> ( K ` C ) ) ) = ( K ` ( G gsumg ( x e. A |-> C ) ) ) )
Theorem	gsummulglem 18341*	Lemma for gsummulg 18342 and gsummulgz 18343. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( G e. Abel \/ N e. NN0 ) )   =>    |- ( ph -> ( G gsumg ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsumg ( k e. A |-> X ) ) ) )
Theorem	gsummulg 18342*	Nonnegative multiple of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( G gsumg ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsumg ( k e. A |-> X ) ) ) )
Theorem	gsummulgz 18343*	Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( G gsumg ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsumg ( k e. A |-> X ) ) ) )
Theorem	gsumzoppg 18344	The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- O = (oppg ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( O gsumg F ) = ( G gsumg F ) )
Theorem	gsumzinv 18345	Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- I = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( I o. F ) ) = ( I ` ( G gsumg F ) ) )
Theorem	gsuminv 18346	Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 4-May-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- I = ( invg ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( I o. F ) ) = ( I ` ( G gsumg F ) ) )
Theorem	gsummptfidminv 18347*	Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- I = ( invg ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- F = ( x e. A |-> C )   =>    |- ( ph -> ( G gsumg ( I o. F ) ) = ( I ` ( G gsumg F ) ) )
Theorem	gsumsub 18348	The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> H : A --> B )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   =>    |- ( ph -> ( G gsumg ( F oF .- H ) ) = ( ( G gsumg F ) .- ( G gsumg H ) ) )
Theorem	gsummptfssub 18349*	The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- ( ph -> F = ( x e. A |-> C ) )   &    |- ( ph -> H = ( x e. A |-> D ) )   &    |- ( ph -> F finSupp .0. )   &    |- ( ph -> H finSupp .0. )   =>    |- ( ph -> ( G gsumg ( x e. A |-> ( C .- D ) ) ) = ( ( G gsumg F ) .- ( G gsumg H ) ) )
Theorem	gsummptfidmsub 18350*	The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- F = ( x e. A |-> C )   &    |- H = ( x e. A |-> D )   =>    |- ( ph -> ( G gsumg ( x e. A |-> ( C .- D ) ) ) = ( ( G gsumg F ) .- ( G gsumg H ) ) )
Theorem	gsumsnfd 18351*	Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. V )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ k = M ) -> A = C )   &    |- F/ k ph   &    |- F/_ k C   =>    |- ( ph -> ( G gsumg ( k e. { M } |-> A ) ) = C )
Theorem	gsumsnd 18352*	Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. V )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ k = M ) -> A = C )   =>    |- ( ph -> ( G gsumg ( k e. { M } |-> A ) ) = C )
Theorem	gsumsnf 18353*	Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
|- F/_ k C   &    |- B = ( Base ` G )   &    |- ( k = M -> A = C )   =>    |- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsumg ( k e. { M } |-> A ) ) = C )
Theorem	gsumsn 18354*	Group sum of a singleton. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- ( k = M -> A = C )   =>    |- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsumg ( k e. { M } |-> A ) ) = C )
Theorem	gsumzunsnd 18355*	Append an element to a finite group sum, more general version of gsumunsnd 18357. (Contributed by AV, 7-Oct-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- Z = (Cntz ` G )   &    |- F = ( k e. ( A u. { M } ) |-> X )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> ran F C_ ( Z ` ran F ) )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. V )   &    |- ( ph -> -. M e. A )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k = M ) -> X = Y )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( k e. A |-> X ) ) .+ Y ) )
Theorem	gsumunsnfd 18356*	Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. V )   &    |- ( ph -> -. M e. A )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k = M ) -> X = Y )   &    |- F/_ k Y   =>    |- ( ph -> ( G gsumg ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsumg ( k e. A |-> X ) ) .+ Y ) )
Theorem	gsumunsnd 18357*	Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 2-Jan-2019.) (Proof shortened by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. V )   &    |- ( ph -> -. M e. A )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k = M ) -> X = Y )   =>    |- ( ph -> ( G gsumg ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsumg ( k e. A |-> X ) ) .+ Y ) )
Theorem	gsumunsnf 18358*	Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
|- F/_ k Y   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. V )   &    |- ( ph -> -. M e. A )   &    |- ( ph -> Y e. B )   &    |- ( k = M -> X = Y )   =>    |- ( ph -> ( G gsumg ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsumg ( k e. A |-> X ) ) .+ Y ) )
Theorem	gsumunsn 18359*	Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Proof shortened by AV, 8-Mar-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. V )   &    |- ( ph -> -. M e. A )   &    |- ( ph -> Y e. B )   &    |- ( k = M -> X = Y )   =>    |- ( ph -> ( G gsumg ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsumg ( k e. A |-> X ) ) .+ Y ) )
Theorem	gsumdifsnd 18360*	Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. W )   &    |- ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. A )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k = M ) -> X = Y )   =>    |- ( ph -> ( G gsumg ( k e. A |-> X ) ) = ( ( G gsumg ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )
Theorem	gsumpt 18361	Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> X e. A )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ( F supp .0. ) C_ { X } )   =>    |- ( ph -> ( G gsumg F ) = ( F ` X ) )
Theorem	gsummptf1o 18362*	Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.)
|- F/_ x H   &    |- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( x = E -> C = H )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> F C_ B )   &    |- ( ( ph /\ x e. A ) -> C e. F )   &    |- ( ( ph /\ y e. D ) -> E e. A )   &    |- ( ( ph /\ x e. A ) -> E! y e. D x = E )   =>    |- ( ph -> ( G gsumg ( x e. A |-> C ) ) = ( G gsumg ( y e. D |-> H ) ) )
Theorem	gsummptun 18363*	Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
|- B = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- .+ = ( +g ` W )   &    |- ( ph -> W e. CMnd )   &    |- ( ph -> ( A u. C ) e. Fin )   &    |- ( ph -> ( A i^i C ) = (/) )   &    |- ( ( ph /\ x e. ( A u. C ) ) -> D e. B )   =>    |- ( ph -> ( W gsumg ( x e. ( A u. C ) |-> D ) ) = ( ( W gsumg ( x e. A |-> D ) ) .+ ( W gsumg ( x e. C |-> D ) ) ) )
Theorem	gsummpt1n0 18364*	If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 18365. (Contributed by AV, 11-Oct-2019.)
|- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> I e. W )   &    |- ( ph -> X e. I )   &    |- F = ( n e. I |-> if ( n = X , A , .0. ) )   &    |- ( ph -> A. n e. I A e. ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = [_ X / n ]_ A )
Theorem	gsummptif1n0 18365*	If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019.) (Proof shortened by AV, 11-Oct-2019.)
|- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> I e. W )   &    |- ( ph -> X e. I )   &    |- F = ( n e. I |-> if ( n = X , A , .0. ) )   &    |- ( ph -> A e. ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = A )
Theorem	gsummptcl 18366*	Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> A. i e. N X e. B )   =>    |- ( ph -> ( G gsumg ( i e. N |-> X ) ) e. B )
Theorem	gsummptfif1o 18367*	Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> A. i e. N X e. B )   &    |- F = ( i e. N |-> X )   &    |- ( ph -> H : C -1-1-onto-> N )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
Theorem	gsummptfzcl 18368*	Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> I = ( M ... N ) )   &    |- ( ph -> A. i e. I X e. B )   =>    |- ( ph -> ( G gsumg ( i e. I |-> X ) ) e. B )
Theorem	gsum2dlem1 18369*	Lemma 1 for gsum2d 18371. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> Rel A )   &    |- ( ph -> D e. W )   &    |- ( ph -> dom A C_ D )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
Theorem	gsum2dlem2 18370*	Lemma for gsum2d 18371. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> Rel A )   &    |- ( ph -> D e. W )   &    |- ( ph -> dom A C_ D )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsumg ( j e. dom ( F supp .0. ) |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
Theorem	gsum2d 18371*	Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> Rel A )   &    |- ( ph -> D e. W )   &    |- ( ph -> dom A C_ D )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
Theorem	gsum2d2lem 18372*	Lemma for gsum2d2 18373: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> C e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )   =>    |- ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )
Theorem	gsum2d2 18373*	Write a group sum over a two-dimensional region as a double sum. (Note that C ( j ) is a function of j.) (Contributed by Mario Carneiro, 28-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> C e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )   =>    |- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) ) )
Theorem	gsumcom2 18374*	Two-dimensional commutation of a group sum. Note that while A and D are constants w.r.t. j , k, C ( j ) and E ( k ) are not. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> C e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )   &    |- ( ph -> D e. Y )   &    |- ( ph -> ( ( j e. A /\ k e. C ) <-> ( k e. D /\ j e. E ) ) )   =>    |- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( k e. D , j e. E |-> X ) ) )
Theorem	gsumxp 18375*	Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ph -> F : ( A X. C ) --> B )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( j e. A |-> ( G gsumg ( k e. C |-> ( j F k ) ) ) ) ) )
Theorem	gsumcom 18376*	Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )   =>    |- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( k e. C , j e. A |-> X ) ) )
Theorem	prdsgsum 18377*	Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` Y )   &    |- ( ph -> I e. V )   &    |- ( ph -> J e. W )   &    |- ( ph -> S e. X )   &    |- ( ( ph /\ x e. I ) -> R e. CMnd )   &    |- ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )   &    |- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )   =>    |- ( ph -> ( Y gsumg ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsumg ( y e. J |-> U ) ) ) )
Theorem	pwsgsum 18378*	Finite commutative sums in a power structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` Y )   &    |- ( ph -> I e. V )   &    |- ( ph -> J e. W )   &    |- ( ph -> R e. CMnd )   &    |- ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )   &    |- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )   =>    |- ( ph -> ( Y gsumg ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsumg ( y e. J |-> U ) ) ) )
10.3.4  Group sums over (ranges of) integers
Theorem	fsfnn0gsumfsffz 18379*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F e. ( B ^m NN0 ) )   &    |- ( ph -> S e. NN0 )   &    |- H = ( F |` ( 0 ... S ) )   =>    |- ( ph -> ( A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) -> ( G gsumg F ) = ( G gsumg H ) ) )
Theorem	nn0gsumfz 18380*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F e. ( B ^m NN0 ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsumg F ) = ( G gsumg f ) ) )
Theorem	nn0gsumfz0 18381*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F e. ( B ^m NN0 ) )   &    |- ( ph -> F finSupp .0. )   =>    |- ( ph -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( G gsumg F ) = ( G gsumg f ) )
Theorem	gsummptnn0fz 18382*	A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.)
|- F/ k ph   &    |- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A. k e. NN0 C e. B )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )   =>    |- ( ph -> ( G gsumg ( k e. NN0 |-> C ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> C ) ) )
Theorem	gsummptnn0fzv 18383*	A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A. k e. NN0 C e. B )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )   =>    |- ( ph -> ( G gsumg ( k e. NN0 |-> C ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> C ) ) )
Theorem	gsummptnn0fzfv 18384*	A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F e. ( B ^m NN0 ) )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) )   =>    |- ( ph -> ( G gsumg ( k e. NN0 |-> ( F ` k ) ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> ( F ` k ) ) ) )
Theorem	telgsumfzslem 18385*	Lemma for telgsumfzs 18386 (induction step). (Contributed by AV, 23-Nov-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   =>    |- ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( G gsumg ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) -> ( G gsumg ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )
Theorem	telgsumfzs 18386*	Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A. k e. ( M ... ( N + 1 ) ) C e. B )   =>    |- ( ph -> ( G gsumg ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) )
Theorem	telgsumfz 18387*	Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 14536. (Contributed by AV, 23-Nov-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A. k e. ( M ... ( N + 1 ) ) A e. B )   &    |- ( k = i -> A = L )   &    |- ( k = ( i + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = ( N + 1 ) -> A = E )   =>    |- ( ph -> ( G gsumg ( i e. ( M ... N ) |-> ( L .- C ) ) ) = ( D .- E ) )
Theorem	telgsumfz0s 18388*	Telescoping finite group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) (Proof shortened by AV, 25-Nov-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. ( 0 ... ( S + 1 ) ) C e. B )   =>    |- ( ph -> ( G gsumg ( i e. ( 0 ... S ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ 0 / k ]_ C .- [_ ( S + 1 ) / k ]_ C ) )
Theorem	telgsumfz0 18389*	Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 14536. (Contributed by AV, 23-Nov-2019.)
|- K = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. ( 0 ... ( S + 1 ) ) A e. K )   &    |- ( k = i -> A = B )   &    |- ( k = ( i + 1 ) -> A = C )   &    |- ( k = 0 -> A = D )   &    |- ( k = ( S + 1 ) -> A = E )   =>    |- ( ph -> ( G gsumg ( i e. ( 0 ... S ) |-> ( B .- C ) ) ) = ( D .- E ) )
Theorem	telgsums 18390*	Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> A. k e. NN0 C e. B )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )   =>    |- ( ph -> ( G gsumg ( i e. NN0 |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = [_ 0 / k ]_ C )
Theorem	telgsum 18391*	Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Abel )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> A. k e. NN0 A e. B )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A. k e. NN0 ( S < k -> A = .0. ) )   &    |- ( k = i -> A = C )   &    |- ( k = ( i + 1 ) -> A = D )   &    |- ( k = 0 -> A = E )   =>    |- ( ph -> ( G gsumg ( i e. NN0 |-> ( C .- D ) ) ) = E )
10.3.5  Internal direct products
Syntax	cdprd 18392	Internal direct product of a family of subgroups.
class DProd
Syntax	cdpj 18393	Projection operator for a direct product.
class dProj
Definition	df-dprd 18394*	Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- DProd = ( g e. Grp , s e. { h | ( h : dom h --> (SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( (Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( (mrCls ` (SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } |-> ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsumg f ) ) )
Definition	df-dpj 18395*	Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- dProj = ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )
Theorem	reldmdprd 18396	The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.)
|- Rel dom DProd
Theorem	dmdprd 18397*	The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.)
|- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( I e. V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> (SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
Theorem	dmdprdd 18398*	Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) )   &    |- ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )   =>    |- ( ph -> G dom DProd S )
Theorem	dprddomprc 18399	A family of subgroups indexed by a proper class cannot be a family of subgroups for an internal direct product. (Contributed by AV, 13-Jul-2019.)
|- ( dom S e/ _V -> -. G dom DProd S )
Theorem	dprddomcld 18400	If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   =>    |- ( ph -> I e. _V )