Metamath Proof Explorer

Theorem prdsgsum

Description: Finite commutative sums in a product 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 prdsgsum.y 
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsgsum.b 
|- B = ( Base ` R )
prdsgsum.z 
|- .0. = ( 0g ` Y )
prdsgsum.i 
|- ( ph -> I e. V )
prdsgsum.j 
|- ( ph -> J e. W )
prdsgsum.s 
|- ( ph -> S e. X )
prdsgsum.r 
|- ( ( ph /\ x e. I ) -> R e. CMnd )
prdsgsum.f 
|- ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )
prdsgsum.w 
|- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
Assertion prdsgsum 
|- ( 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 prdsgsum.y 
 |-  Y = ( S Xs_ ( x e. I |-> R ) )
2 prdsgsum.b 
 |-  B = ( Base ` R )
3 prdsgsum.z 
 |-  .0. = ( 0g ` Y )
4 prdsgsum.i 
 |-  ( ph -> I e. V )
5 prdsgsum.j 
 |-  ( ph -> J e. W )
6 prdsgsum.s 
 |-  ( ph -> S e. X )
7 prdsgsum.r 
 |-  ( ( ph /\ x e. I ) -> R e. CMnd )
8 prdsgsum.f 
 |-  ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )
9 prdsgsum.w 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 7 fmpttd 
 |-  ( ph -> ( x e. I |-> R ) : I --> CMnd )
12 11 ffnd 
 |-  ( ph -> ( x e. I |-> R ) Fn I )
13 1 4 6 11 prdscmnd 
 |-  ( ph -> Y e. CMnd )
14 8 anassrs 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> U e. B )
15 14 an32s 
 |-  ( ( ( ph /\ y e. J ) /\ x e. I ) -> U e. B )
16 15 ralrimiva 
 |-  ( ( ph /\ y e. J ) -> A. x e. I U e. B )
17 7 ralrimiva 
 |-  ( ph -> A. x e. I R e. CMnd )
18 1 10 6 4 17 2 prdsbasmpt2 
 |-  ( ph -> ( ( x e. I |-> U ) e. ( Base ` Y ) <-> A. x e. I U e. B ) )
19 18 adantr 
 |-  ( ( ph /\ y e. J ) -> ( ( x e. I |-> U ) e. ( Base ` Y ) <-> A. x e. I U e. B ) )
20 16 19 mpbird 
 |-  ( ( ph /\ y e. J ) -> ( x e. I |-> U ) e. ( Base ` Y ) )
21 20 fmpttd 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) : J --> ( Base ` Y ) )
22 10 3 13 5 21 9 gsumcl 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) e. ( Base ` Y ) )
23 1 10 6 4 12 22 prdsbasfn 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) Fn I )
24 nfcv 
 |-  F/_ x Y
25 nfcv 
 |-  F/_ x gsum
26 nfcv 
 |-  F/_ x J
27 nfmpt1 
 |-  F/_ x ( x e. I |-> U )
28 26 27 nfmpt 
 |-  F/_ x ( y e. J |-> ( x e. I |-> U ) )
29 24 25 28 nfov 
 |-  F/_ x ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) )
30 29 dffn5f 
 |-  ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) Fn I <-> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) ) )
31 23 30 sylib 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) ) )
32 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
33 eqid 
 |-  ( x e. I |-> U ) = ( x e. I |-> U )
34 33 fvmpt2 
 |-  ( ( x e. I /\ U e. B ) -> ( ( x e. I |-> U ) ` x ) = U )
35 32 14 34 syl2an2r 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( ( x e. I |-> U ) ` x ) = U )
36 35 mpteq2dva 
 |-  ( ( ph /\ x e. I ) -> ( y e. J |-> ( ( x e. I |-> U ) ` x ) ) = ( y e. J |-> U ) )
37 36 oveq2d 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> ( ( x e. I |-> U ) ` x ) ) ) = ( R gsum ( y e. J |-> U ) ) )
38 13 adantr 
 |-  ( ( ph /\ x e. I ) -> Y e. CMnd )
39 cmnmnd 
 |-  ( R e. CMnd -> R e. Mnd )
40 7 39 syl 
 |-  ( ( ph /\ x e. I ) -> R e. Mnd )
41 5 adantr 
 |-  ( ( ph /\ x e. I ) -> J e. W )
42 4 adantr 
 |-  ( ( ph /\ x e. I ) -> I e. V )
43 6 adantr 
 |-  ( ( ph /\ x e. I ) -> S e. X )
44 40 fmpttd 
 |-  ( ph -> ( x e. I |-> R ) : I --> Mnd )
45 44 adantr 
 |-  ( ( ph /\ x e. I ) -> ( x e. I |-> R ) : I --> Mnd )
46 1 10 42 43 45 32 prdspjmhm 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( Base ` Y ) |-> ( a ` x ) ) e. ( Y MndHom ( ( x e. I |-> R ) ` x ) ) )
47 eqid 
 |-  ( x e. I |-> R ) = ( x e. I |-> R )
48 47 fvmpt2 
 |-  ( ( x e. I /\ R e. CMnd ) -> ( ( x e. I |-> R ) ` x ) = R )
49 32 7 48 syl2anc 
 |-  ( ( ph /\ x e. I ) -> ( ( x e. I |-> R ) ` x ) = R )
50 49 oveq2d 
 |-  ( ( ph /\ x e. I ) -> ( Y MndHom ( ( x e. I |-> R ) ` x ) ) = ( Y MndHom R ) )
51 46 50 eleqtrd 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( Base ` Y ) |-> ( a ` x ) ) e. ( Y MndHom R ) )
52 20 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( x e. I |-> U ) e. ( Base ` Y ) )
53 9 adantr 
 |-  ( ( ph /\ x e. I ) -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
54 fveq1 
 |-  ( a = ( x e. I |-> U ) -> ( a ` x ) = ( ( x e. I |-> U ) ` x ) )
55 fveq1 
 |-  ( a = ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) -> ( a ` x ) = ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) )
56 10 3 38 40 41 51 52 53 54 55 gsummhm2 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> ( ( x e. I |-> U ) ` x ) ) ) = ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) )
57 37 56 eqtr3d 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> U ) ) = ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) )
58 57 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) = ( x e. I |-> ( ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) ` x ) ) )
59 31 58 eqtr4d 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )