Theorem gsummulg

Description: 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)

	Ref	Expression
Hypotheses	gsummulg.b	$$⊢B={\mathrm{Base}}_G$$
	gsummulg.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummulg.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	gsummulg.a	$$⊢\phi \to A\in V$$
	gsummulg.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsummulg.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
	gsummulg.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummulg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	gsummulg	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_G},X\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummulg.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummulg.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummulg.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		gsummulg.a	$$⊢\phi \to A\in V$$
5		gsummulg.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
6		gsummulg.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
7		gsummulg.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
8		gsummulg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9	8	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
10	8	olcd	$$⊢\phi \to \left(G\in \mathrm{Abel}\vee N\in {\mathbb{N}}_0\right)$$
11	1 2 3 4 5 6 7 9 10	gsummulglem	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_G},X\right)$$