This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 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 ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )