Step | Hyp | Ref
| Expression |
1 | | psrbag.d |
. . . 4
|
2 | | psrbagconf1o.1 |
. . . 4
|
3 | | gsumbagdiag.i |
. . . 4
|
4 | | gsumbagdiag.f |
. . . 4
|
5 | | gsumbagdiag.b |
. . . 4
|
6 | | gsumbagdiag.g |
. . . 4
CMnd |
7 | 1, 2, 3, 4 | gsumbagdiaglem 19375 |
. . . . 5
|
8 | | gsumbagdiag.x |
. . . . . . . . . . . 12
|
9 | 8 | anassrs 680 |
. . . . . . . . . . 11
|
10 | | eqid 2622 |
. . . . . . . . . . 11
|
11 | 9, 10 | fmptd 6385 |
. . . . . . . . . 10
|
12 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
13 | | ssrab2 3687 |
. . . . . . . . . . . . . 14
|
14 | 2, 13 | eqsstri 3635 |
. . . . . . . . . . . . 13
|
15 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
|
16 | | simpr 477 |
. . . . . . . . . . . . . 14
|
17 | 1, 2 | psrbagconcl 19373 |
. . . . . . . . . . . . . 14
|
18 | 12, 15, 16, 17 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
19 | 14, 18 | sseldi 3601 |
. . . . . . . . . . . 12
|
20 | | eqid 2622 |
. . . . . . . . . . . . 13
|
21 | 1, 20 | psrbagconf1o 19374 |
. . . . . . . . . . . 12
|
22 | 12, 19, 21 | syl2anc 693 |
. . . . . . . . . . 11
|
23 | | f1of 6137 |
. . . . . . . . . . 11
|
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
|
25 | | fco 6058 |
. . . . . . . . . 10
|
26 | 11, 24, 25 | syl2anc 693 |
. . . . . . . . 9
|
27 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
28 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
29 | 1 | psrbagf 19365 |
. . . . . . . . . . . . . . . . 17
|
30 | 27, 28, 29 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
32 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
33 | 14, 32 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
34 | 1 | psrbagf 19365 |
. . . . . . . . . . . . . . . . 17
|
35 | 27, 33, 34 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
37 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
|
38 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
39 | 37, 38 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
40 | 1 | psrbagf 19365 |
. . . . . . . . . . . . . . . . 17
|
41 | 27, 39, 40 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
43 | | nn0cn 11302 |
. . . . . . . . . . . . . . . 16
|
44 | | nn0cn 11302 |
. . . . . . . . . . . . . . . 16
|
45 | | nn0cn 11302 |
. . . . . . . . . . . . . . . 16
|
46 | | sub32 10315 |
. . . . . . . . . . . . . . . 16
|
47 | 43, 44, 45, 46 | syl3an 1368 |
. . . . . . . . . . . . . . 15
|
48 | 31, 36, 42, 47 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
49 | 48 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
|
50 | | ovexd 6680 |
. . . . . . . . . . . . . 14
|
51 | 30 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
|
52 | 35 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
|
53 | 27, 31, 36, 51, 52 | offval2 6914 |
. . . . . . . . . . . . . 14
|
54 | 41 | feqmptd 6249 |
. . . . . . . . . . . . . 14
|
55 | 27, 50, 42, 53, 54 | offval2 6914 |
. . . . . . . . . . . . 13
|
56 | | ovexd 6680 |
. . . . . . . . . . . . . 14
|
57 | 27, 31, 42, 51, 54 | offval2 6914 |
. . . . . . . . . . . . . 14
|
58 | 27, 56, 36, 57, 52 | offval2 6914 |
. . . . . . . . . . . . 13
|
59 | 49, 55, 58 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
60 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
61 | 1, 20 | psrbagconcl 19373 |
. . . . . . . . . . . . 13
|
62 | 27, 60, 38, 61 | syl3anc 1326 |
. . . . . . . . . . . 12
|
63 | 59, 62 | eqeltrrd 2702 |
. . . . . . . . . . 11
|
64 | 59 | mpteq2dva 4744 |
. . . . . . . . . . 11
|
65 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
66 | | nfcsb1v 3549 |
. . . . . . . . . . . . 13
|
67 | | csbeq1a 3542 |
. . . . . . . . . . . . 13
|
68 | 65, 66, 67 | cbvmpt 4749 |
. . . . . . . . . . . 12
|
69 | 68 | a1i 11 |
. . . . . . . . . . 11
|
70 | | csbeq1 3536 |
. . . . . . . . . . 11
|
71 | 63, 64, 69, 70 | fmptco 6396 |
. . . . . . . . . 10
|
72 | 71 | feq1d 6030 |
. . . . . . . . 9
|
73 | 26, 72 | mpbid 222 |
. . . . . . . 8
|
74 | | eqid 2622 |
. . . . . . . . 9
|
75 | 74 | fmpt 6381 |
. . . . . . . 8
|
76 | 73, 75 | sylibr 224 |
. . . . . . 7
|
77 | 76 | r19.21bi 2932 |
. . . . . 6
|
78 | 77 | anasss 679 |
. . . . 5
|
79 | 7, 78 | syldan 487 |
. . . 4
|
80 | 1, 2, 3, 4, 5, 6, 79 | gsumbagdiag 19376 |
. . 3
g
g
|
81 | | eqid 2622 |
. . . 4
|
82 | 1 | psrbaglefi 19372 |
. . . . . 6
|
83 | 3, 4, 82 | syl2anc 693 |
. . . . 5
|
84 | 2, 83 | syl5eqel 2705 |
. . . 4
|
85 | 3 | adantr 481 |
. . . . 5
|
86 | 4 | adantr 481 |
. . . . . . 7
|
87 | | simpr 477 |
. . . . . . 7
|
88 | 1, 2 | psrbagconcl 19373 |
. . . . . . 7
|
89 | 85, 86, 87, 88 | syl3anc 1326 |
. . . . . 6
|
90 | 14, 89 | sseldi 3601 |
. . . . 5
|
91 | 1 | psrbaglefi 19372 |
. . . . 5
|
92 | 85, 90, 91 | syl2anc 693 |
. . . 4
|
93 | | xpfi 8231 |
. . . . 5
|
94 | 84, 84, 93 | syl2anc 693 |
. . . 4
|
95 | | simprl 794 |
. . . . . . 7
|
96 | 7 | simpld 475 |
. . . . . . 7
|
97 | | brxp 5147 |
. . . . . . 7
|
98 | 95, 96, 97 | sylanbrc 698 |
. . . . . 6
|
99 | 98 | pm2.24d 147 |
. . . . 5
|
100 | 99 | impr 649 |
. . . 4
|
101 | 5, 81, 6, 84, 92, 79, 94, 100 | gsum2d2 18373 |
. . 3
g
g g |
102 | 1 | psrbaglefi 19372 |
. . . . 5
|
103 | 12, 19, 102 | syl2anc 693 |
. . . 4
|
104 | | simprl 794 |
. . . . . . 7
|
105 | 1, 2, 3, 4 | gsumbagdiaglem 19375 |
. . . . . . . 8
|
106 | 105 | simpld 475 |
. . . . . . 7
|
107 | | brxp 5147 |
. . . . . . 7
|
108 | 104, 106,
107 | sylanbrc 698 |
. . . . . 6
|
109 | 108 | pm2.24d 147 |
. . . . 5
|
110 | 109 | impr 649 |
. . . 4
|
111 | 5, 81, 6, 84, 103, 78, 94, 110 | gsum2d2 18373 |
. . 3
g
g g |
112 | 80, 101, 111 | 3eqtr3d 2664 |
. 2
g g g g
|
113 | 6 | adantr 481 |
. . . . . . . 8
CMnd |
114 | 79 | anassrs 680 |
. . . . . . . . 9
|
115 | | eqid 2622 |
. . . . . . . . 9
|
116 | 114, 115 | fmptd 6385 |
. . . . . . . 8
|
117 | | ovex 6678 |
. . . . . . . . . . . 12
|
118 | 1, 117 | rabex2 4815 |
. . . . . . . . . . 11
|
119 | 118 | a1i 11 |
. . . . . . . . . 10
|
120 | | rabexg 4812 |
. . . . . . . . . 10
|
121 | | mptexg 6484 |
. . . . . . . . . 10
|
122 | 119, 120,
121 | 3syl 18 |
. . . . . . . . 9
|
123 | | funmpt 5926 |
. . . . . . . . . 10
|
124 | 123 | a1i 11 |
. . . . . . . . 9
|
125 | | fvexd 6203 |
. . . . . . . . 9
|
126 | | suppssdm 7308 |
. . . . . . . . . . 11
supp |
127 | 115 | dmmptss 5631 |
. . . . . . . . . . 11
|
128 | 126, 127 | sstri 3612 |
. . . . . . . . . 10
supp |
129 | 128 | a1i 11 |
. . . . . . . . 9
supp |
130 | | suppssfifsupp 8290 |
. . . . . . . . 9
supp
finSupp |
131 | 122, 124,
125, 92, 129, 130 | syl32anc 1334 |
. . . . . . . 8
finSupp |
132 | 5, 81, 113, 92, 116, 131 | gsumcl 18316 |
. . . . . . 7
g |
133 | | eqid 2622 |
. . . . . . 7
g g |
134 | 132, 133 | fmptd 6385 |
. . . . . 6
g |
135 | 1, 2 | psrbagconf1o 19374 |
. . . . . . . 8
|
136 | 3, 4, 135 | syl2anc 693 |
. . . . . . 7
|
137 | | f1ocnv 6149 |
. . . . . . 7
|
138 | | f1of 6137 |
. . . . . . 7
|
139 | 136, 137,
138 | 3syl 18 |
. . . . . 6
|
140 | | fco 6058 |
. . . . . 6
g
g
|
141 | 134, 139,
140 | syl2anc 693 |
. . . . 5
g
|
142 | | coass 5654 |
. . . . . . . 8
g
g
|
143 | | f1ococnv2 6163 |
. . . . . . . . . 10
|
144 | 136, 143 | syl 17 |
. . . . . . . . 9
|
145 | 144 | coeq2d 5284 |
. . . . . . . 8
g
g |
146 | 142, 145 | syl5eq 2668 |
. . . . . . 7
g
g |
147 | | eqidd 2623 |
. . . . . . . . 9
|
148 | | eqidd 2623 |
. . . . . . . . 9
g g |
149 | | breq2 4657 |
. . . . . . . . . . . 12
|
150 | 149 | rabbidv 3189 |
. . . . . . . . . . 11
|
151 | | ovex 6678 |
. . . . . . . . . . . . 13
|
152 | | psrass1lem.y |
. . . . . . . . . . . . 13
|
153 | 151, 152 | csbie 3559 |
. . . . . . . . . . . 12
|
154 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
155 | 154 | csbeq1d 3540 |
. . . . . . . . . . . 12
|
156 | 153, 155 | syl5eqr 2670 |
. . . . . . . . . . 11
|
157 | 150, 156 | mpteq12dv 4733 |
. . . . . . . . . 10
|
158 | 157 | oveq2d 6666 |
. . . . . . . . 9
g g
|
159 | 89, 147, 148, 158 | fmptco 6396 |
. . . . . . . 8
g
g |
160 | 159 | coeq1d 5283 |
. . . . . . 7
g
g
|
161 | | coires1 5653 |
. . . . . . . . 9
g g
|
162 | | ssid 3624 |
. . . . . . . . . 10
|
163 | | resmpt 5449 |
. . . . . . . . . 10
g
g
|
164 | 162, 163 | ax-mp 5 |
. . . . . . . . 9
g
g
|
165 | 161, 164 | eqtri 2644 |
. . . . . . . 8
g g |
166 | 165 | a1i 11 |
. . . . . . 7
g
g |
167 | 146, 160,
166 | 3eqtr3d 2664 |
. . . . . 6
g
g |
168 | 167 | feq1d 6030 |
. . . . 5
g
g |
169 | 141, 168 | mpbid 222 |
. . . 4
g |
170 | | rabexg 4812 |
. . . . . . . 8
|
171 | 118, 170 | mp1i 13 |
. . . . . . 7
|
172 | 2, 171 | syl5eqel 2705 |
. . . . . 6
|
173 | | mptexg 6484 |
. . . . . 6
g |
174 | 172, 173 | syl 17 |
. . . . 5
g |
175 | | funmpt 5926 |
. . . . . 6
g |
176 | 175 | a1i 11 |
. . . . 5
g
|
177 | | fvexd 6203 |
. . . . 5
|
178 | | suppssdm 7308 |
. . . . . . 7
g supp g |
179 | | eqid 2622 |
. . . . . . . 8
g g |
180 | 179 | dmmptss 5631 |
. . . . . . 7
g
|
181 | 178, 180 | sstri 3612 |
. . . . . 6
g supp |
182 | 181 | a1i 11 |
. . . . 5
g
supp |
183 | | suppssfifsupp 8290 |
. . . . 5
g
g
g supp g finSupp |
184 | 174, 176,
177, 84, 182, 183 | syl32anc 1334 |
. . . 4
g finSupp |
185 | 5, 81, 6, 84, 169, 184, 136 | gsumf1o 18317 |
. . 3
g g g g
|
186 | 159 | oveq2d 6666 |
. . 3
g g
g g |
187 | 185, 186 | eqtrd 2656 |
. 2
g g g g |
188 | 6 | adantr 481 |
. . . . . 6
CMnd |
189 | 118 | a1i 11 |
. . . . . . . 8
|
190 | | rabexg 4812 |
. . . . . . . 8
|
191 | | mptexg 6484 |
. . . . . . . 8
|
192 | 189, 190,
191 | 3syl 18 |
. . . . . . 7
|
193 | | funmpt 5926 |
. . . . . . . 8
|
194 | 193 | a1i 11 |
. . . . . . 7
|
195 | | fvexd 6203 |
. . . . . . 7
|
196 | | suppssdm 7308 |
. . . . . . . . 9
supp |
197 | 10 | dmmptss 5631 |
. . . . . . . . 9
|
198 | 196, 197 | sstri 3612 |
. . . . . . . 8
supp
|
199 | 198 | a1i 11 |
. . . . . . 7
supp
|
200 | | suppssfifsupp 8290 |
. . . . . . 7
supp
finSupp |
201 | 192, 194,
195, 103, 199, 200 | syl32anc 1334 |
. . . . . 6
finSupp |
202 | 5, 81, 188, 103, 11, 201, 22 | gsumf1o 18317 |
. . . . 5
g g
|
203 | 71 | oveq2d 6666 |
. . . . 5
g
g |
204 | 202, 203 | eqtrd 2656 |
. . . 4
g g
|
205 | 204 | mpteq2dva 4744 |
. . 3
g g |
206 | 205 | oveq2d 6666 |
. 2
g g g g |
207 | 112, 187,
206 | 3eqtr4d 2666 |
1
g g g g |