gsummulc2

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019)

	Ref	Expression
Hypotheses	gsummulc1.b	$⊢ B = {Base}_{R}$
	gsummulc1.z	$⊢ \underset{˙}{0} = 0_{R}$
	gsummulc1.p	$⊢ \underset{˙}{+} = +_{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)$

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

Metamath Proof Explorer