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 ^s I )
pwsgsum.b 
|- B = ( Base ` R )
pwsgsum.z 
|- .0. = ( 0g ` Y )
pwsgsum.i 
|- ( ph -> I e. V )
pwsgsum.j 
|- ( ph -> J e. W )
pwsgsum.r 
|- ( ph -> R e. CMnd )
pwsgsum.f 
|- ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )
pwsgsum.w 
|- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
Assertion pwsgsum 
|- ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )

Proof

Step Hyp Ref Expression
1 pwsgsum.y 
 |-  Y = ( R ^s I )
2 pwsgsum.b 
 |-  B = ( Base ` R )
3 pwsgsum.z 
 |-  .0. = ( 0g ` Y )
4 pwsgsum.i 
 |-  ( ph -> I e. V )
5 pwsgsum.j 
 |-  ( ph -> J e. W )
6 pwsgsum.r 
 |-  ( ph -> R e. CMnd )
7 pwsgsum.f 
 |-  ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )
8 pwsgsum.w 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
9 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
10 1 9 pwsval 
 |-  ( ( R e. CMnd /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
11 6 4 10 syl2anc 
 |-  ( ph -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
12 11 oveq1d 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) )
13 fconstmpt 
 |-  ( I X. { R } ) = ( x e. I |-> R )
14 13 oveq2i 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( x e. I |-> R ) )
15 eqid 
 |-  ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
16 fvexd 
 |-  ( ph -> ( Scalar ` R ) e. _V )
17 6 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. CMnd )
18 11 fveq2d 
 |-  ( ph -> ( 0g ` Y ) = ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
19 3 18 eqtrid 
 |-  ( ph -> .0. = ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
20 8 19 breqtrd 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
21 14 2 15 4 5 16 17 7 20 prdsgsum 
 |-  ( ph -> ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )
22 12 21 eqtrd 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )