Theorem gsummulgz

Description: Integer multiple of a group sum. (Contributed 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)$$
	gsummulgz.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsummulgz.n	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	gsummulgz	$$⊢\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		gsummulgz.g	$$⊢\phi \to G\in \mathrm{Abel}$$
8		gsummulgz.n	$$⊢\phi \to N\in \mathbb{Z}$$
9		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
10	7 9	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
11	7	orcd	$$⊢\phi \to \left(G\in \mathrm{Abel}\vee N\in {\mathbb{N}}_0\right)$$
12	1 2 3 4 5 6 10 8 11	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)$$