Metamath Proof Explorer

Theorem gsummulc2

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) Remove unused hypothesis. (Revised by SN, 7-Mar-2025)

		Ref	Expression
	Hypotheses	gsummulc1.b	$⊢ B = {Base}_{R}$
		gsummulc1.z	$⊢ \underset{˙}{0} = 0_{R}$
		gsummulc1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		gsummulc1.r	$⊢ φ \to R \in Ring$
		gsummulc1.a	$⊢ φ \to A \in V$
		gsummulc1.y	$⊢ φ \to Y \in B$
		gsummulc1.x	$⊢ (φ \land k \in A) \to X \in B$
		gsummulc1.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
	Assertion	gsummulc2	$⊢ φ \to \underset{k \in A}{\sum_{R}} (Y \underset{˙}{\cdot} X) = Y \underset{˙}{\cdot} (\underset{k \in A}{\sum_{R}}, X)$

Proof

Step	Hyp	Ref	Expression
1		gsummulc1.b	$⊢ B = {Base}_{R}$
2		gsummulc1.z	$⊢ \underset{˙}{0} = 0_{R}$
3		gsummulc1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		gsummulc1.r	$⊢ φ \to R \in Ring$
5		gsummulc1.a	$⊢ φ \to A \in V$
6		gsummulc1.y	$⊢ φ \to Y \in B$
7		gsummulc1.x	$⊢ (φ \land k \in A) \to X \in B$
8		gsummulc1.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
9	4	ringcmnd	$⊢ φ \to R \in CMnd$
10		ringmnd	$⊢ R \in Ring \to R \in Mnd$
11	4 10	syl	$⊢ φ \to R \in Mnd$
12	1 3	ringlghm	$⊢ (R \in Ring \land Y \in B) \to (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R GrpHom R)$
13	4 6 12	syl2anc	$⊢ φ \to (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R GrpHom R)$
14		ghmmhm	$⊢ (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R GrpHom R) \to (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R MndHom R)$
15	13 14	syl	$⊢ φ \to (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R MndHom R)$
16		oveq2	$⊢ x = X \to Y \underset{˙}{\cdot} x = Y \underset{˙}{\cdot} X$
17		oveq2	$⊢ x = \underset{k \in A}{\sum_{R}} X \to Y \underset{˙}{\cdot} x = Y \underset{˙}{\cdot} (\underset{k \in A}{\sum_{R}}, X)$
18	1 2 9 11 5 15 7 8 16 17	gsummhm2	$⊢ φ \to \underset{k \in A}{\sum_{R}} (Y \underset{˙}{\cdot} X) = Y \underset{˙}{\cdot} (\underset{k \in A}{\sum_{R}}, X)$