Theorem gsummulgc2

Description: A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsummulgc1.b	$$⊢B={\mathrm{Base}}_M$$
	gsummulgc1.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	gsummulgc1.r	$$⊢\phi \to M\in \mathrm{Grp}$$
	gsummulgc1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummulgc1.y	$$⊢\phi \to Y\in B$$
	gsummulgc1.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in \mathbb{Z}$$
Assertion	gsummulgc2	$$⊢\phi \to \underset{k\in A}{{\sum }_M}\left(X\underset{\dot{}}{·}Y\right)=\sum _{k\in A}X\underset{\dot{}}{·}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsummulgc1.b	$$⊢B={\mathrm{Base}}_M$$
2		gsummulgc1.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
3		gsummulgc1.r	$$⊢\phi \to M\in \mathrm{Grp}$$
4		gsummulgc1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsummulgc1.y	$$⊢\phi \to Y\in B$$
6		gsummulgc1.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in \mathbb{Z}$$
7		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
8		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
9		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
10		ringcmn	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CMnd}$$
11	9 10	mp1i	$$⊢\phi \to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CMnd}$$
12	3	grpmndd	$$⊢\phi \to M\in \mathrm{Mnd}$$
13		eqid	$$⊢\left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)=\left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)$$
14	2 13 1	mulgghm2	$$⊢\left(M\in \mathrm{Grp}\wedge Y\in B\right)\to \left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}M\right)$$
15	3 5 14	syl2anc	$$⊢\phi \to \left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}M\right)$$
16		ghmmhm	$$⊢\left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}M\right)\to \left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{MndHom}M\right)$$
17	15 16	syl	$$⊢\phi \to \left(x\in \mathbb{Z}⟼x\underset{\dot{}}{·}Y\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{MndHom}M\right)$$
18		eqid	$$⊢\left(k\in A⟼X\right)=\left(k\in A⟼X\right)$$
19		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
20	18 4 6 19	fsuppmptdm	$$⊢\phi \to {finSupp}_0\left(\left(k\in A⟼X\right)\right)$$
21		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y$$
22		oveq1	$$⊢x=\underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}}X\to x\underset{\dot{}}{·}Y=\left(\underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}},X\right)\underset{\dot{}}{·}Y$$
23	7 8 11 12 4 17 6 20 21 22	gsummhm2	$$⊢\phi \to \underset{k\in A}{{\sum }_M}\left(X\underset{\dot{}}{·}Y\right)=\left(\underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}},X\right)\underset{\dot{}}{·}Y$$
24	4 6	gsumzrsum	$$⊢\phi \to \underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}}X=\sum _{k\in A}X$$
25	24	oveq1d	$$⊢\phi \to \left(\underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}},X\right)\underset{\dot{}}{·}Y=\sum _{k\in A}X\underset{\dot{}}{·}Y$$
26	23 25	eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }_M}\left(X\underset{\dot{}}{·}Y\right)=\sum _{k\in A}X\underset{\dot{}}{·}Y$$