gsumvsmul

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 , since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 5-May-2015) (Revised by AV, 10-Jul-2019)

	Ref	Expression
Hypotheses	gsumvsmul.b	$⊢ B = {Base}_{R}$
	gsumvsmul.s	$⊢ S = Scalar (R)$
	gsumvsmul.k	$⊢ K = {Base}_{S}$
	gsumvsmul.z	$⊢ \underset{˙}{0} = 0_{R}$
	gsumvsmul.p	$⊢ \underset{˙}{+} = +_{R}$
	gsumvsmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	gsumvsmul.r	$⊢ φ \to R \in LMod$
	gsumvsmul.a	$⊢ φ \to A \in V$
	gsumvsmul.x	$⊢ φ \to X \in K$
	gsumvsmul.y	$⊢ (φ \land k \in A) \to Y \in B$
	gsumvsmul.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ Y))$
Assertion	gsumvsmul	$⊢ φ \to \underset{k \in A}{\sum_{R}} (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} (\underset{k \in A}{\sum_{R}}, Y)$

Proof

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

Metamath Proof Explorer

Theorem gsumvsmul

Proof