Theorem pwsgsum

Description: Finite commutative sums in a power structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 3-Jul-2015) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	pwsgsum.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsgsum.b	$$⊢B={\mathrm{Base}}_R$$
	pwsgsum.z	$$⊢\underset{\dot{}}{0}=0_Y$$
	pwsgsum.i	$$⊢\phi \to I\in V$$
	pwsgsum.j	$$⊢\phi \to J\in W$$
	pwsgsum.r	$$⊢\phi \to R\in \mathrm{CMnd}$$
	pwsgsum.f	$$⊢\left(\phi \wedge \left(x\in I\wedge y\in J\right)\right)\to U\in B$$
	pwsgsum.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in J⟼\left(x\in I⟼U\right)\right)\right)$$
Assertion	pwsgsum	$$⊢\phi \to \underset{y\in J}{{\sum }_Y}\left(x\in I⟼U\right)=\left(x\in I⟼\underset{y\in J}{{\sum }_R}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwsgsum.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsgsum.b	$$⊢B={\mathrm{Base}}_R$$
3		pwsgsum.z	$$⊢\underset{\dot{}}{0}=0_Y$$
4		pwsgsum.i	$$⊢\phi \to I\in V$$
5		pwsgsum.j	$$⊢\phi \to J\in W$$
6		pwsgsum.r	$$⊢\phi \to R\in \mathrm{CMnd}$$
7		pwsgsum.f	$$⊢\left(\phi \wedge \left(x\in I\wedge y\in J\right)\right)\to U\in B$$
8		pwsgsum.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in J⟼\left(x\in I⟼U\right)\right)\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
10	1 9	pwsval	$$⊢\left(R\in \mathrm{CMnd}\wedge I\in V\right)\to Y=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
11	6 4 10	syl2anc	$$⊢\phi \to Y=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
12	11	oveq1d	$$⊢\phi \to \underset{y\in J}{{\sum }_Y}\left(x\in I⟼U\right)=\underset{y\in J}{{\sum }_{\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)}}\left(x\in I⟼U\right)$$
13		fconstmpt	$$⊢I\times \left\{R\right\}=\left(x\in I⟼R\right)$$
14	13	oveq2i	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(x\in I⟼R\right)$$
15		eqid	$$⊢0_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}=0_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
16		fvexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right)\in \mathrm{V}$$
17	6	adantr	$$⊢\left(\phi \wedge x\in I\right)\to R\in \mathrm{CMnd}$$
18	11	fveq2d	$$⊢\phi \to 0_Y=0_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
19	3 18	syl5eq	$$⊢\phi \to \underset{\dot{}}{0}=0_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
20	8 19	breqtrd	$$⊢\phi \to {finSupp}_{0_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}}\left(\left(y\in J⟼\left(x\in I⟼U\right)\right)\right)$$
21	14 2 15 4 5 16 17 7 20	prdsgsum	$$⊢\phi \to \underset{y\in J}{{\sum }_{\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)}}\left(x\in I⟼U\right)=\left(x\in I⟼\underset{y\in J}{{\sum }_R}U\right)$$
22	12 21	eqtrd	$$⊢\phi \to \underset{y\in J}{{\sum }_Y}\left(x\in I⟼U\right)=\left(x\in I⟼\underset{y\in J}{{\sum }_R}U\right)$$