gsumvsmul1

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 , since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023)

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

Proof

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

Metamath Proof Explorer

Theorem gsumvsmul1

Proof