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 Y = R 𝑠 I
pwsgsum.b B = Base R
pwsgsum.z 0 ˙ = 0 Y
pwsgsum.i φ I V
pwsgsum.j φ J W
pwsgsum.r φ R CMnd
pwsgsum.f φ x I y J U B
pwsgsum.w φ finSupp 0 ˙ y J x I U
Assertion pwsgsum φ Y y J x I U = x I R y J U

Proof

Step Hyp Ref Expression
1 pwsgsum.y Y = R 𝑠 I
2 pwsgsum.b B = Base R
3 pwsgsum.z 0 ˙ = 0 Y
4 pwsgsum.i φ I V
5 pwsgsum.j φ J W
6 pwsgsum.r φ R CMnd
7 pwsgsum.f φ x I y J U B
8 pwsgsum.w φ finSupp 0 ˙ y J x I U
9 eqid Scalar R = Scalar R
10 1 9 pwsval R CMnd I V Y = Scalar R 𝑠 I × R
11 6 4 10 syl2anc φ Y = Scalar R 𝑠 I × R
12 11 oveq1d φ Y y J x I U = Scalar R 𝑠 I × R y J x I U
13 fconstmpt I × R = x I R
14 13 oveq2i Scalar R 𝑠 I × R = Scalar R 𝑠 x I R
15 eqid 0 Scalar R 𝑠 I × R = 0 Scalar R 𝑠 I × R
16 fvexd φ Scalar R V
17 6 adantr φ x I R CMnd
18 11 fveq2d φ 0 Y = 0 Scalar R 𝑠 I × R
19 3 18 syl5eq φ 0 ˙ = 0 Scalar R 𝑠 I × R
20 8 19 breqtrd φ finSupp 0 Scalar R 𝑠 I × R y J x I U
21 14 2 15 4 5 16 17 7 20 prdsgsum φ Scalar R 𝑠 I × R y J x I U = x I R y J U
22 12 21 eqtrd φ Y y J x I U = x I R y J U