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	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsgsum.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pwsgsum.z	⊢ 0 = ( 0g ‘ 𝑌 )
	pwsgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	pwsgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
	pwsgsum.r	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	pwsgsum.f	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
	pwsgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
Assertion	pwsgsum	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwsgsum.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsgsum.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		pwsgsum.z	⊢ 0 = ( 0g ‘ 𝑌 )
4		pwsgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		pwsgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
6		pwsgsum.r	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
7		pwsgsum.f	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
8		pwsgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
9		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
10	1 9	pwsval	⊢ ( ( 𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
11	6 4 10	syl2anc	⊢ ( 𝜑 → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
12	11	oveq1d	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) )
13		fconstmpt	⊢ ( 𝐼 × { 𝑅 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
14	13	oveq2i	⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
15		eqid	⊢ ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
16		fvexd	⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
17	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CMnd )
18	11	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑌 ) = ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
19	3 18	syl5eq	⊢ ( 𝜑 → 0 = ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
20	8 19	breqtrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
21	14 2 15 4 5 16 17 7 20	prdsgsum	⊢ ( 𝜑 → ( ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )
22	12 21	eqtrd	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )