Step | Hyp | Ref
| Expression |
1 | | tsmsf1o.s |
. . . . . . . . . . 11
|
2 | | f1opwfi 8270 |
. . . . . . . . . . 11
|
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
|
4 | | f1of 6137 |
. . . . . . . . . 10
|
5 | 3, 4 | syl 17 |
. . . . . . . . 9
|
6 | | eqid 2622 |
. . . . . . . . . 10
|
7 | 6 | fmpt 6381 |
. . . . . . . . 9
|
8 | 5, 7 | sylibr 224 |
. . . . . . . 8
|
9 | | sseq1 3626 |
. . . . . . . . . . 11
|
10 | 9 | imbi1d 331 |
. . . . . . . . . 10
g g |
11 | 10 | ralbidv 2986 |
. . . . . . . . 9
g g |
12 | 6, 11 | rexrnmpt 6369 |
. . . . . . . 8
g g |
13 | 8, 12 | syl 17 |
. . . . . . 7
g g |
14 | | f1ofo 6144 |
. . . . . . . . 9
|
15 | | forn 6118 |
. . . . . . . . 9
|
16 | 3, 14, 15 | 3syl 18 |
. . . . . . . 8
|
17 | 16 | rexeqdv 3145 |
. . . . . . 7
g g |
18 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
|
19 | 18 | cbvmptv 4750 |
. . . . . . . . . . . . . 14
|
20 | 19 | fmpt 6381 |
. . . . . . . . . . . . 13
|
21 | 5, 20 | sylibr 224 |
. . . . . . . . . . . 12
|
22 | | sseq2 3627 |
. . . . . . . . . . . . . 14
|
23 | | reseq2 5391 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
g g |
25 | 24 | eleq1d 2686 |
. . . . . . . . . . . . . 14
g g |
26 | 22, 25 | imbi12d 334 |
. . . . . . . . . . . . 13
g g |
27 | 19, 26 | ralrnmpt 6368 |
. . . . . . . . . . . 12
g g |
28 | 21, 27 | syl 17 |
. . . . . . . . . . 11
g g |
29 | 16 | raleqdv 3144 |
. . . . . . . . . . 11
g g |
30 | 28, 29 | bitr3d 270 |
. . . . . . . . . 10
g
g |
31 | 30 | adantr 481 |
. . . . . . . . 9
g
g |
32 | | f1of1 6136 |
. . . . . . . . . . . . . 14
|
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . 13
|
34 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
|
35 | | elfpw 8268 |
. . . . . . . . . . . . . 14
|
36 | 35 | simplbi 476 |
. . . . . . . . . . . . 13
|
37 | 36 | ad2antlr 763 |
. . . . . . . . . . . 12
|
38 | | elfpw 8268 |
. . . . . . . . . . . . . 14
|
39 | 38 | simplbi 476 |
. . . . . . . . . . . . 13
|
40 | 39 | adantl 482 |
. . . . . . . . . . . 12
|
41 | | f1imass 6521 |
. . . . . . . . . . . 12
|
42 | 34, 37, 40, 41 | syl12anc 1324 |
. . . . . . . . . . 11
|
43 | | tsmsf1o.b |
. . . . . . . . . . . . . 14
|
44 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
45 | | tsmsf1o.1 |
. . . . . . . . . . . . . . 15
CMnd |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . 14
CMnd |
47 | 38 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
48 | 47 | adantl 482 |
. . . . . . . . . . . . . . 15
|
49 | | f1ores 6151 |
. . . . . . . . . . . . . . . . 17
|
50 | 34, 40, 49 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
51 | | f1ofo 6144 |
. . . . . . . . . . . . . . . 16
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
|
53 | | fofi 8252 |
. . . . . . . . . . . . . . 15
|
54 | 48, 52, 53 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
55 | | tsmsf1o.f |
. . . . . . . . . . . . . . . 16
|
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
57 | | imassrn 5477 |
. . . . . . . . . . . . . . . 16
|
58 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
59 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . 17
|
60 | | forn 6118 |
. . . . . . . . . . . . . . . . 17
|
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
62 | 57, 61 | syl5sseq 3653 |
. . . . . . . . . . . . . . 15
|
63 | 56, 62 | fssresd 6071 |
. . . . . . . . . . . . . 14
|
64 | | fvexd 6203 |
. . . . . . . . . . . . . . 15
|
65 | 63, 54, 64 | fdmfifsupp 8285 |
. . . . . . . . . . . . . 14
finSupp |
66 | 43, 44, 46, 54, 63, 65, 50 | gsumf1o 18317 |
. . . . . . . . . . . . 13
g g |
67 | | df-ima 5127 |
. . . . . . . . . . . . . . . . 17
|
68 | 67 | eqimss2i 3660 |
. . . . . . . . . . . . . . . 16
|
69 | | cores 5638 |
. . . . . . . . . . . . . . . 16
|
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
71 | | resco 5639 |
. . . . . . . . . . . . . . 15
|
72 | 70, 71 | eqtr4i 2647 |
. . . . . . . . . . . . . 14
|
73 | 72 | oveq2i 6661 |
. . . . . . . . . . . . 13
g g |
74 | 66, 73 | syl6eq 2672 |
. . . . . . . . . . . 12
g g |
75 | 74 | eleq1d 2686 |
. . . . . . . . . . 11
g
g |
76 | 42, 75 | imbi12d 334 |
. . . . . . . . . 10
g g |
77 | 76 | ralbidva 2985 |
. . . . . . . . 9
g
g |
78 | 31, 77 | bitr3d 270 |
. . . . . . . 8
g g |
79 | 78 | rexbidva 3049 |
. . . . . . 7
g
g |
80 | 13, 17, 79 | 3bitr3d 298 |
. . . . . 6
g
g |
81 | 80 | imbi2d 330 |
. . . . 5
g
g |
82 | 81 | ralbidv 2986 |
. . . 4
g
g |
83 | 82 | anbi2d 740 |
. . 3
g
g |
84 | | eqid 2622 |
. . . 4
|
85 | | eqid 2622 |
. . . 4
|
86 | | tsmsf1o.2 |
. . . 4
|
87 | | tsmsf1o.a |
. . . 4
|
88 | 43, 84, 85, 45, 86, 87, 55 | eltsms 21936 |
. . 3
tsums
g |
89 | | eqid 2622 |
. . . 4
|
90 | | f1dmex 7136 |
. . . . 5
|
91 | 33, 87, 90 | syl2anc 693 |
. . . 4
|
92 | | f1of 6137 |
. . . . . 6
|
93 | 1, 92 | syl 17 |
. . . . 5
|
94 | | fco 6058 |
. . . . 5
|
95 | 55, 93, 94 | syl2anc 693 |
. . . 4
|
96 | 43, 84, 89, 45, 86, 91, 95 | eltsms 21936 |
. . 3
tsums
g |
97 | 83, 88, 96 | 3bitr4d 300 |
. 2
tsums
tsums |
98 | 97 | eqrdv 2620 |
1
tsums tsums
|