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 | |
|
prdsgsum.b | |
||
prdsgsum.z | |
||
prdsgsum.i | |
||
prdsgsum.j | |
||
prdsgsum.s | |
||
prdsgsum.r | |
||
prdsgsum.f | |
||
prdsgsum.w | |
||
Assertion | prdsgsum | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prdsgsum.y | |
|
2 | prdsgsum.b | |
|
3 | prdsgsum.z | |
|
4 | prdsgsum.i | |
|
5 | prdsgsum.j | |
|
6 | prdsgsum.s | |
|
7 | prdsgsum.r | |
|
8 | prdsgsum.f | |
|
9 | prdsgsum.w | |
|
10 | eqid | |
|
11 | 7 | fmpttd | |
12 | 11 | ffnd | |
13 | 1 4 6 11 | prdscmnd | |
14 | 8 | anassrs | |
15 | 14 | an32s | |
16 | 15 | ralrimiva | |
17 | 7 | ralrimiva | |
18 | 1 10 6 4 17 2 | prdsbasmpt2 | |
19 | 18 | adantr | |
20 | 16 19 | mpbird | |
21 | 20 | fmpttd | |
22 | 10 3 13 5 21 9 | gsumcl | |
23 | 1 10 6 4 12 22 | prdsbasfn | |
24 | nfcv | |
|
25 | nfcv | |
|
26 | nfcv | |
|
27 | nfmpt1 | |
|
28 | 26 27 | nfmpt | |
29 | 24 25 28 | nfov | |
30 | 29 | dffn5f | |
31 | 23 30 | sylib | |
32 | simpr | |
|
33 | eqid | |
|
34 | 33 | fvmpt2 | |
35 | 32 14 34 | syl2an2r | |
36 | 35 | mpteq2dva | |
37 | 36 | oveq2d | |
38 | 13 | adantr | |
39 | cmnmnd | |
|
40 | 7 39 | syl | |
41 | 5 | adantr | |
42 | 4 | adantr | |
43 | 6 | adantr | |
44 | 40 | fmpttd | |
45 | 44 | adantr | |
46 | 1 10 42 43 45 32 | prdspjmhm | |
47 | eqid | |
|
48 | 47 | fvmpt2 | |
49 | 32 7 48 | syl2anc | |
50 | 49 | oveq2d | |
51 | 46 50 | eleqtrd | |
52 | 20 | adantlr | |
53 | 9 | adantr | |
54 | fveq1 | |
|
55 | fveq1 | |
|
56 | 10 3 38 40 41 51 52 53 54 55 | gsummhm2 | |
57 | 37 56 | eqtr3d | |
58 | 57 | mpteq2dva | |
59 | 31 58 | eqtr4d | |