Step | Hyp | Ref
| Expression |
1 | | tsmssubm.s |
. . . . . 6
SubMnd |
2 | | tsmssubm.h |
. . . . . . 7
↾s |
3 | 2 | submbas 17355 |
. . . . . 6
SubMnd
|
4 | 1, 3 | syl 17 |
. . . . 5
|
5 | 4 | eleq2d 2687 |
. . . 4
|
6 | 5 | anbi1d 741 |
. . 3
g
g |
7 | | elin 3796 |
. . . . 5
tsums tsums |
8 | | ancom 466 |
. . . . 5
tsums
tsums |
9 | 7, 8 | bitri 264 |
. . . 4
tsums tsums |
10 | | eqid 2622 |
. . . . . . . . . 10
|
11 | 10 | submss 17350 |
. . . . . . . . 9
SubMnd
|
12 | 1, 11 | syl 17 |
. . . . . . . 8
|
13 | 12 | sselda 3603 |
. . . . . . 7
|
14 | | eqid 2622 |
. . . . . . . . 9
|
15 | | eqid 2622 |
. . . . . . . . 9
|
16 | | tsmssubm.1 |
. . . . . . . . 9
CMnd |
17 | | tsmssubm.2 |
. . . . . . . . 9
|
18 | | tsmssubm.a |
. . . . . . . . 9
|
19 | | tsmssubm.f |
. . . . . . . . . 10
|
20 | 19, 12 | fssd 6057 |
. . . . . . . . 9
|
21 | 10, 14, 15, 16, 17, 18, 20 | eltsms 21936 |
. . . . . . . 8
tsums
g |
22 | 21 | baibd 948 |
. . . . . . 7
tsums
g |
23 | 13, 22 | syldan 487 |
. . . . . 6
tsums
g |
24 | | vex 3203 |
. . . . . . . . 9
|
25 | 24 | inex1 4799 |
. . . . . . . 8
|
26 | 25 | a1i 11 |
. . . . . . 7
|
27 | 2, 14 | resstopn 20990 |
. . . . . . . . 9
↾t |
28 | 27 | eleq2i 2693 |
. . . . . . . 8
↾t
|
29 | | fvex 6201 |
. . . . . . . . . 10
|
30 | | elrest 16088 |
. . . . . . . . . 10
SubMnd
↾t
|
31 | 29, 1, 30 | sylancr 695 |
. . . . . . . . 9
↾t |
32 | 31 | adantr 481 |
. . . . . . . 8
↾t
|
33 | 28, 32 | syl5bbr 274 |
. . . . . . 7
|
34 | | eleq2 2690 |
. . . . . . . . 9
|
35 | | elin 3796 |
. . . . . . . . . . 11
|
36 | 35 | rbaib 947 |
. . . . . . . . . 10
|
37 | 36 | adantl 482 |
. . . . . . . . 9
|
38 | 34, 37 | sylan9bbr 737 |
. . . . . . . 8
|
39 | | eleq2 2690 |
. . . . . . . . . . . . 13
g g |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
41 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
42 | 2 | submmnd 17354 |
. . . . . . . . . . . . . . . . . . . 20
SubMnd
|
43 | 1, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 2 | subcmn 18242 |
. . . . . . . . . . . . . . . . . . 19
CMnd CMnd |
45 | 16, 43, 44 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
CMnd |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
CMnd |
47 | | elfpw 8268 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 47 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
50 | 19 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 47 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 50, 52 | fssresd 6071 |
. . . . . . . . . . . . . . . . . 18
|
54 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | feq3d 6032 |
. . . . . . . . . . . . . . . . . 18
|
56 | 53, 55 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
57 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
59 | 53, 49, 58 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . . . 17
finSupp |
60 | 40, 41, 46, 49, 56, 59 | gsumcl 18316 |
. . . . . . . . . . . . . . . 16
g |
61 | 60, 54 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
g |
62 | | elin 3796 |
. . . . . . . . . . . . . . . 16
g g g
|
63 | 62 | rbaib 947 |
. . . . . . . . . . . . . . 15
g g g |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . 14
g g |
65 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
SubMnd |
66 | 49, 65, 53, 2 | gsumsubm 17373 |
. . . . . . . . . . . . . . 15
g g |
67 | 66 | eleq1d 2686 |
. . . . . . . . . . . . . 14
g g |
68 | 64, 67 | bitr4d 271 |
. . . . . . . . . . . . 13
g g |
69 | 39, 68 | sylan9bbr 737 |
. . . . . . . . . . . 12
g g |
70 | 69 | an32s 846 |
. . . . . . . . . . 11
g g |
71 | 70 | imbi2d 330 |
. . . . . . . . . 10
g g |
72 | 71 | ralbidva 2985 |
. . . . . . . . 9
g
g |
73 | 72 | rexbidv 3052 |
. . . . . . . 8
g
g |
74 | 38, 73 | imbi12d 334 |
. . . . . . 7
g
g |
75 | 26, 33, 74 | ralxfr2d 4882 |
. . . . . 6
g
g |
76 | 23, 75 | bitr4d 271 |
. . . . 5
tsums
g |
77 | 76 | pm5.32da 673 |
. . . 4
tsums g |
78 | 9, 77 | syl5bb 272 |
. . 3
tsums
g |
79 | | eqid 2622 |
. . . 4
|
80 | | resstps 20991 |
. . . . . 6
SubMnd
↾s |
81 | 17, 1, 80 | syl2anc 693 |
. . . . 5
↾s |
82 | 2, 81 | syl5eqel 2705 |
. . . 4
|
83 | 4 | feq3d 6032 |
. . . . 5
|
84 | 19, 83 | mpbid 222 |
. . . 4
|
85 | 40, 79, 15, 45, 82, 18, 84 | eltsms 21936 |
. . 3
tsums
g |
86 | 6, 78, 85 | 3bitr4rd 301 |
. 2
tsums
tsums
|
87 | 86 | eqrdv 2620 |
1
tsums tsums |