Proof of Theorem gsum2d
Step | Hyp | Ref
| Expression |
1 | | gsum2d.b |
. . 3
     |
2 | | gsum2d.z |
. . 3
     |
3 | | gsum2d.g |
. . 3
 CMnd |
4 | | gsum2d.a |
. . 3
   |
5 | | gsum2d.r |
. . 3
   |
6 | | gsum2d.d |
. . 3
   |
7 | | gsum2d.s |
. . 3
   |
8 | | gsum2d.f |
. . 3
       |
9 | | gsum2d.w |
. . 3
 finSupp
 |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem2 17681 |
. 2
  g    supp     g  
supp  g                  |
11 | | suppssdm 6946 |
. . . . . 6
 supp  |
12 | | fdm 5745 |
. . . . . . 7
       |
13 | 8, 12 | syl 17 |
. . . . . 6
   |
14 | 11, 13 | syl5sseq 3466 |
. . . . 5
  supp   |
15 | | relss 4927 |
. . . . . . 7
  supp
  supp    |
16 | 14, 5, 15 | sylc 61 |
. . . . . 6
  supp   |
17 | | relssdmrn 5363 |
. . . . . . 7
  supp  supp   supp 
supp    |
18 | | ssv 3438 |
. . . . . . . 8
 supp  |
19 | | xpss2 4949 |
. . . . . . . 8
  supp   supp 
supp    supp    |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
  supp  supp    supp   |
21 | 17, 20 | syl6ss 3430 |
. . . . . 6
  supp  supp   supp    |
22 | 16, 21 | syl 17 |
. . . . 5
  supp   supp    |
23 | 14, 22 | ssind 3647 |
. . . 4
  supp    supp     |
24 | | df-res 4851 |
. . . 4
  supp     supp    |
25 | 23, 24 | syl6sseqr 3465 |
. . 3
  supp   supp    |
26 | 1, 2, 3, 4, 8, 25,
9 | gsumres 17625 |
. 2
  g    supp     g    |
27 | | dmss 5039 |
. . . . . . 7
  supp
 supp
  |
28 | 14, 27 | syl 17 |
. . . . . 6
  supp   |
29 | 28, 7 | sstrd 3428 |
. . . . 5
  supp   |
30 | 29 | resmptd 5162 |
. . . 4
    g                supp    supp  g                 |
31 | 30 | oveq2d 6324 |
. . 3
  g    g                supp    g  
supp  g                  |
32 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem1 17680 |
. . . . . 6
  g                |
33 | 32 | adantr 472 |
. . . . 5
 
  g                |
34 | | eqid 2471 |
. . . . 5
  g                 g                |
35 | 33, 34 | fmptd 6061 |
. . . 4
   g                     |
36 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
37 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
38 | 36, 37 | elimasn 5199 |
. . . . . . . . . . . . 13
            |
39 | 38 | biimpi 199 |
. . . . . . . . . . . 12
            |
40 | 39 | ad2antll 743 |
. . . . . . . . . . 11
 
  
supp               |
41 | | eldifn 3545 |
. . . . . . . . . . . . 13
   supp 
 supp   |
42 | 41 | ad2antrl 742 |
. . . . . . . . . . . 12
 
  
supp         
 supp   |
43 | 36, 37 | opeldm 5044 |
. . . . . . . . . . . 12
     supp  supp   |
44 | 42, 43 | nsyl 125 |
. . . . . . . . . . 11
 
  
supp         
  
 supp   |
45 | 40, 44 | eldifd 3401 |
. . . . . . . . . 10
 
  
supp               supp
   |
46 | | df-ov 6311 |
. . . . . . . . . . 11
            |
47 | | ssid 3437 |
. . . . . . . . . . . . 13
 supp  supp  |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
  supp  supp   |
49 | | fvex 5889 |
. . . . . . . . . . . . . 14
     |
50 | 2, 49 | eqeltri 2545 |
. . . . . . . . . . . . 13
 |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
   |
52 | 8, 48, 4, 51 | suppssr 6965 |
. . . . . . . . . . 11
 
  
  supp           |
53 | 46, 52 | syl5eq 2517 |
. . . . . . . . . 10
 
  
  supp        |
54 | 45, 53 | syldan 478 |
. . . . . . . . 9
 
  
supp               |
55 | 54 | anassrs 660 |
. . . . . . . 8
    
supp               |
56 | 55 | mpteq2dva 4482 |
. . . . . . 7
 

 supp                        |
57 | 56 | oveq2d 6324 |
. . . . . 6
 

 supp    g               g           |
58 | | cmnmnd 17523 |
. . . . . . . . 9
 CMnd   |
59 | 3, 58 | syl 17 |
. . . . . . . 8
   |
60 | | imaexg 6749 |
. . . . . . . . 9
         |
61 | 4, 60 | syl 17 |
. . . . . . . 8
         |
62 | 2 | gsumz 16699 |
. . . . . . . 8
          g          |
63 | 59, 61, 62 | syl2anc 673 |
. . . . . . 7
  g          |
64 | 63 | adantr 472 |
. . . . . 6
 

 supp    g          |
65 | 57, 64 | eqtrd 2505 |
. . . . 5
 

 supp    g               |
66 | 65, 6 | suppss2 6968 |
. . . 4
    g               supp 
supp   |
67 | | funmpt 5625 |
. . . . . 6
  g                |
68 | 67 | a1i 11 |
. . . . 5
   g                 |
69 | 9 | fsuppimpd 7908 |
. . . . . . 7
  supp   |
70 | | dmfi 7872 |
. . . . . . 7
  supp
 supp   |
71 | 69, 70 | syl 17 |
. . . . . 6
  supp
  |
72 | | ssfi 7810 |
. . . . . 6
   supp
   g               supp  supp     g               supp   |
73 | 71, 66, 72 | syl2anc 673 |
. . . . 5
    g               supp   |
74 | | mptexg 6151 |
. . . . . . 7
   g                 |
75 | 6, 74 | syl 17 |
. . . . . 6
   g                 |
76 | | isfsupp 7905 |
. . . . . 6
    g                   g               finSupp    g                  g               supp     |
77 | 75, 51, 76 | syl2anc 673 |
. . . . 5
    g               finSupp    g                  g               supp     |
78 | 68, 73, 77 | mpbir2and 936 |
. . . 4
   g               finSupp  |
79 | 1, 2, 3, 6, 35, 66, 78 | gsumres 17625 |
. . 3
  g    g                supp    g   g                  |
80 | 31, 79 | eqtr3d 2507 |
. 2
  g  
supp  g                 g   g                  |
81 | 10, 26, 80 | 3eqtr3d 2513 |
1
  g   g   g                  |