gsummulc2OLD

Description: Obsolete version of gsummulc2 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		gsummulc1OLD.b	$⊢ B = {Base}_{R}$
2		gsummulc1OLD.z	$⊢ \underset{˙}{0} = 0_{R}$
3		gsummulc1OLD.p	$⊢ \underset{˙}{+} = +_{R}$
4		gsummulc1OLD.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		gsummulc1OLD.r	$⊢ φ \to R \in Ring$
6		gsummulc1OLD.a	$⊢ φ \to A \in V$
7		gsummulc1OLD.y	$⊢ φ \to Y \in B$
8		gsummulc1OLD.x	$⊢ (φ \land k \in A) \to X \in B$
9		gsummulc1OLD.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

Theorem gsummulc2OLD

Proof