sgsummulcl

Description: A finite semiring sum multiplied by a constant, analogous to gsummulc2 . (Contributed by AV, 23-Aug-2019)

	Ref	Expression
Hypotheses	srgsummulcr.b	$⊢ B = {Base}_{R}$
	srgsummulcr.z	$⊢ \underset{˙}{0} = 0_{R}$
	srgsummulcr.p	$⊢ \underset{˙}{+} = +_{R}$
	srgsummulcr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	srgsummulcr.r	$⊢ φ \to R \in SRing$
	srgsummulcr.a	$⊢ φ \to A \in V$
	srgsummulcr.y	$⊢ φ \to Y \in B$
	srgsummulcr.x	$⊢ (φ \land k \in A) \to X \in B$
	srgsummulcr.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
Assertion	sgsummulcl	$⊢ φ \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		srgsummulcr.b	$⊢ B = {Base}_{R}$
2		srgsummulcr.z	$⊢ \underset{˙}{0} = 0_{R}$
3		srgsummulcr.p	$⊢ \underset{˙}{+} = +_{R}$
4		srgsummulcr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		srgsummulcr.r	$⊢ φ \to R \in SRing$
6		srgsummulcr.a	$⊢ φ \to A \in V$
7		srgsummulcr.y	$⊢ φ \to Y \in B$
8		srgsummulcr.x	$⊢ (φ \land k \in A) \to X \in B$
9		srgsummulcr.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
10		srgcmn	$⊢ R \in SRing \to R \in CMnd$
11	5 10	syl	$⊢ φ \to R \in CMnd$
12		srgmnd	$⊢ R \in SRing \to R \in Mnd$
13	5 12	syl	$⊢ φ \to R \in Mnd$
14	1 4	srglmhm	$⊢ (R \in SRing \land Y \in B) \to (x \in B ⟼ Y \underset{˙}{\cdot} x) \in (R MndHom R)$
15	5 7 14	syl2anc	$⊢ φ \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 11 13 6 15 8 9 16 17	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