Metamath Proof Explorer

Theorem gsummulc1

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	gsummulc1	$⊢ φ \to \underset{k \in A}{\sum_{R}} (X \underset{˙}{\cdot} Y) = (\underset{k \in A}{\sum_{R}}, X) \underset{˙}{\cdot} Y$

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	ringrghm	$⊢ (R \in Ring \land Y \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} Y) \in (R GrpHom R)$
13	4 6 12	syl2anc	$⊢ φ \to (x \in B ⟼ x \underset{˙}{\cdot} Y) \in (R GrpHom R)$
14		ghmmhm	$⊢ (x \in B ⟼ x \underset{˙}{\cdot} Y) \in (R GrpHom R) \to (x \in B ⟼ x \underset{˙}{\cdot} Y) \in (R MndHom R)$
15	13 14	syl	$⊢ φ \to (x \in B ⟼ x \underset{˙}{\cdot} Y) \in (R MndHom R)$
16		oveq1	$⊢ x = X \to x \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Y$
17		oveq1	$⊢ x = \underset{k \in A}{\sum_{R}} X \to x \underset{˙}{\cdot} Y = (\underset{k \in A}{\sum_{R}}, X) \underset{˙}{\cdot} Y$
18	1 2 9 11 5 15 7 8 16 17	gsummhm2	$⊢ φ \to \underset{k \in A}{\sum_{R}} (X \underset{˙}{\cdot} Y) = (\underset{k \in A}{\sum_{R}}, X) \underset{˙}{\cdot} Y$