Step | Hyp | Ref
| Expression |
1 | | gsum2d2.b |
. . 3
|
2 | | gsum2d2.z |
. . 3
|
3 | | gsum2d2.g |
. . 3
CMnd |
4 | | gsum2d2.a |
. . . 4
|
5 | | snex 4908 |
. . . . . 6
|
6 | | gsum2d2.r |
. . . . . 6
|
7 | | xpexg 6960 |
. . . . . 6
|
8 | 5, 6, 7 | sylancr 695 |
. . . . 5
|
9 | 8 | ralrimiva 2966 |
. . . 4
|
10 | | iunexg 7143 |
. . . 4
|
11 | 4, 9, 10 | syl2anc 693 |
. . 3
|
12 | | gsum2d2.f |
. . . . 5
|
13 | 12 | ralrimivva 2971 |
. . . 4
|
14 | | eqid 2622 |
. . . . 5
|
15 | 14 | fmpt2x 7236 |
. . . 4
|
16 | 13, 15 | sylib 208 |
. . 3
|
17 | | gsum2d2.u |
. . . 4
|
18 | | gsum2d2.n |
. . . 4
|
19 | 1, 2, 3, 4, 6, 12,
17, 18 | gsum2d2lem 18372 |
. . 3
finSupp |
20 | | relxp 5227 |
. . . . . . 7
|
21 | 20 | rgenw 2924 |
. . . . . 6
|
22 | | reliun 5239 |
. . . . . 6
|
23 | 21, 22 | mpbir 221 |
. . . . 5
|
24 | | cnvf1o 7276 |
. . . . 5
|
25 | 23, 24 | ax-mp 5 |
. . . 4
|
26 | | relxp 5227 |
. . . . . . . 8
|
27 | 26 | rgenw 2924 |
. . . . . . 7
|
28 | | reliun 5239 |
. . . . . . 7
|
29 | 27, 28 | mpbir 221 |
. . . . . 6
|
30 | | relcnv 5503 |
. . . . . 6
|
31 | | nfv 1843 |
. . . . . . . 8
|
32 | | nfv 1843 |
. . . . . . . . 9
|
33 | | nfiu1 4550 |
. . . . . . . . . . 11
|
34 | 33 | nfcnv 5301 |
. . . . . . . . . 10
|
35 | 34 | nfel2 2781 |
. . . . . . . . 9
|
36 | 32, 35 | nfbi 1833 |
. . . . . . . 8
|
37 | 31, 36 | nfim 1825 |
. . . . . . 7
|
38 | | opeq2 4403 |
. . . . . . . . . 10
|
39 | 38 | eleq1d 2686 |
. . . . . . . . 9
|
40 | 38 | eleq1d 2686 |
. . . . . . . . 9
|
41 | 39, 40 | bibi12d 335 |
. . . . . . . 8
|
42 | 41 | imbi2d 330 |
. . . . . . 7
|
43 | | nfv 1843 |
. . . . . . . . 9
|
44 | | nfiu1 4550 |
. . . . . . . . . . 11
|
45 | 44 | nfel2 2781 |
. . . . . . . . . 10
|
46 | | nfv 1843 |
. . . . . . . . . 10
|
47 | 45, 46 | nfbi 1833 |
. . . . . . . . 9
|
48 | 43, 47 | nfim 1825 |
. . . . . . . 8
|
49 | | opeq1 4402 |
. . . . . . . . . . 11
|
50 | 49 | eleq1d 2686 |
. . . . . . . . . 10
|
51 | 49 | eleq1d 2686 |
. . . . . . . . . 10
|
52 | 50, 51 | bibi12d 335 |
. . . . . . . . 9
|
53 | 52 | imbi2d 330 |
. . . . . . . 8
|
54 | | gsumcom2.c |
. . . . . . . . . 10
|
55 | | opeliunxp 5170 |
. . . . . . . . . 10
|
56 | | opeliunxp 5170 |
. . . . . . . . . 10
|
57 | 54, 55, 56 | 3bitr4g 303 |
. . . . . . . . 9
|
58 | | vex 3203 |
. . . . . . . . . 10
|
59 | | vex 3203 |
. . . . . . . . . 10
|
60 | 58, 59 | opelcnv 5304 |
. . . . . . . . 9
|
61 | 57, 60 | syl6bbr 278 |
. . . . . . . 8
|
62 | 48, 53, 61 | chvar 2262 |
. . . . . . 7
|
63 | 37, 42, 62 | chvar 2262 |
. . . . . 6
|
64 | 29, 30, 63 | eqrelrdv 5216 |
. . . . 5
|
65 | | f1oeq3 6129 |
. . . . 5
|
66 | 64, 65 | syl 17 |
. . . 4
|
67 | 25, 66 | mpbiri 248 |
. . 3
|
68 | 1, 2, 3, 11, 16, 19, 67 | gsumf1o 18317 |
. 2
g
g
|
69 | | sneq 4187 |
. . . . . . . . . . 11
|
70 | 69 | cnveqd 5298 |
. . . . . . . . . 10
|
71 | 70 | unieqd 4446 |
. . . . . . . . 9
|
72 | | opswap 5622 |
. . . . . . . . 9
|
73 | 71, 72 | syl6eq 2672 |
. . . . . . . 8
|
74 | 73 | fveq2d 6195 |
. . . . . . 7
|
75 | | df-ov 6653 |
. . . . . . 7
|
76 | 74, 75 | syl6eqr 2674 |
. . . . . 6
|
77 | 76 | mpt2mptx 6751 |
. . . . 5
|
78 | | nfcv 2764 |
. . . . . . 7
|
79 | | nfcv 2764 |
. . . . . . . 8
|
80 | | nfcsb1v 3549 |
. . . . . . . 8
|
81 | 79, 80 | nfxp 5142 |
. . . . . . 7
|
82 | | sneq 4187 |
. . . . . . . 8
|
83 | | csbeq1a 3542 |
. . . . . . . 8
|
84 | 82, 83 | xpeq12d 5140 |
. . . . . . 7
|
85 | 78, 81, 84 | cbviun 4557 |
. . . . . 6
|
86 | | mpteq1 4737 |
. . . . . 6
|
87 | 85, 86 | ax-mp 5 |
. . . . 5
|
88 | | nfcv 2764 |
. . . . . 6
|
89 | | nfcv 2764 |
. . . . . 6
|
90 | | nfcv 2764 |
. . . . . 6
|
91 | | nfcv 2764 |
. . . . . . 7
|
92 | | nfmpt22 6723 |
. . . . . . 7
|
93 | | nfcv 2764 |
. . . . . . 7
|
94 | 91, 92, 93 | nfov 6676 |
. . . . . 6
|
95 | | nfcv 2764 |
. . . . . . 7
|
96 | | nfmpt21 6722 |
. . . . . . 7
|
97 | | nfcv 2764 |
. . . . . . 7
|
98 | 95, 96, 97 | nfov 6676 |
. . . . . 6
|
99 | | oveq2 6658 |
. . . . . . 7
|
100 | | oveq1 6657 |
. . . . . . 7
|
101 | 99, 100 | sylan9eq 2676 |
. . . . . 6
|
102 | 88, 80, 89, 90, 94, 98, 83, 101 | cbvmpt2x 6733 |
. . . . 5
|
103 | 77, 87, 102 | 3eqtr4i 2654 |
. . . 4
|
104 | | f1of 6137 |
. . . . . . 7
|
105 | 67, 104 | syl 17 |
. . . . . 6
|
106 | | eqid 2622 |
. . . . . . 7
|
107 | 106 | fmpt 6381 |
. . . . . 6
|
108 | 105, 107 | sylibr 224 |
. . . . 5
|
109 | | eqidd 2623 |
. . . . 5
|
110 | 16 | feqmptd 6249 |
. . . . 5
|
111 | | fveq2 6191 |
. . . . 5
|
112 | 108, 109,
110, 111 | fmptcof 6397 |
. . . 4
|
113 | 12 | ex 450 |
. . . . . . . . 9
|
114 | 14 | ovmpt4g 6783 |
. . . . . . . . . 10
|
115 | 114 | 3expia 1267 |
. . . . . . . . 9
|
116 | 113, 115 | sylcom 30 |
. . . . . . . 8
|
117 | 54, 116 | sylbird 250 |
. . . . . . 7
|
118 | 117 | 3impib 1262 |
. . . . . 6
|
119 | 118 | eqcomd 2628 |
. . . . 5
|
120 | 119 | mpt2eq3dva 6719 |
. . . 4
|
121 | 103, 112,
120 | 3eqtr4a 2682 |
. . 3
|
122 | 121 | oveq2d 6666 |
. 2
g
g
|
123 | 68, 122 | eqtrd 2656 |
1
g
g
|