Theorem gsummulc1OLD

Description: Obsolete version of gsummulc1 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={\mathrm{Base}}_R$$
	gsummulc1OLD.z	$$⊢\underset{\dot{}}{0}=0_R$$
	gsummulc1OLD.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	gsummulc1OLD.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	gsummulc1OLD.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	gsummulc1OLD.a	$$⊢\phi \to A\in V$$
	gsummulc1OLD.y	$$⊢\phi \to Y\in B$$
	gsummulc1OLD.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsummulc1OLD.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
Assertion	gsummulc1OLD	$$⊢\phi \to \underset{k\in A}{{\sum }_R}\left(X\underset{\dot{}}{·}Y\right)=\left(\underset{k\in A}{{\sum }_R},X\right)\underset{\dot{}}{·}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsummulc1OLD.b	$$⊢B={\mathrm{Base}}_R$$
2		gsummulc1OLD.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		gsummulc1OLD.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		gsummulc1OLD.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		gsummulc1OLD.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		gsummulc1OLD.a	$$⊢\phi \to A\in V$$
7		gsummulc1OLD.y	$$⊢\phi \to Y\in B$$
8		gsummulc1OLD.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
9		gsummulc1OLD.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
10		ringcmn	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$
11	5 10	syl	$$⊢\phi \to R\in \mathrm{CMnd}$$
12		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
13	5 12	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
14	1 4	ringrghm	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to \left(x\in B⟼x\underset{\dot{}}{·}Y\right)\in \left(R\mathrm{GrpHom}R\right)$$
15	5 7 14	syl2anc	$$⊢\phi \to \left(x\in B⟼x\underset{\dot{}}{·}Y\right)\in \left(R\mathrm{GrpHom}R\right)$$
16		ghmmhm	$$⊢\left(x\in B⟼x\underset{\dot{}}{·}Y\right)\in \left(R\mathrm{GrpHom}R\right)\to \left(x\in B⟼x\underset{\dot{}}{·}Y\right)\in \left(R\mathrm{MndHom}R\right)$$
17	15 16	syl	$$⊢\phi \to \left(x\in B⟼x\underset{\dot{}}{·}Y\right)\in \left(R\mathrm{MndHom}R\right)$$
18		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y$$
19		oveq1	$$⊢x=\underset{k\in A}{{\sum }_R}X\to x\underset{\dot{}}{·}Y=\left(\underset{k\in A}{{\sum }_R},X\right)\underset{\dot{}}{·}Y$$
20	1 2 11 13 6 17 8 9 18 19	gsummhm2	$$⊢\phi \to \underset{k\in A}{{\sum }_R}\left(X\underset{\dot{}}{·}Y\right)=\left(\underset{k\in A}{{\sum }_R},X\right)\underset{\dot{}}{·}Y$$