Step | Hyp | Ref
| Expression |
1 | | mptscmfsupp0.d |
. . 3
   |
2 | | mptexg 6121 |
. . 3
       |
3 | 1, 2 | syl 17 |
. 2
       |
4 | | funmpt 5597 |
. . 3
     |
5 | 4 | a1i 11 |
. 2
       |
6 | | mptscmfsupp0.0 |
. . . 4
     |
7 | | fvex 5858 |
. . . 4
     |
8 | 6, 7 | eqeltri 2526 |
. . 3
 |
9 | 8 | a1i 11 |
. 2
   |
10 | | mptscmfsupp0.f |
. . 3
   finSupp   |
11 | 10 | fsuppimpd 7877 |
. 2
    supp    |
12 | | simpr 467 |
. . . . . . . 8
 
   |
13 | | mptscmfsupp0.s |
. . . . . . . . . . 11
 
   |
14 | 13 | ralrimiva 2790 |
. . . . . . . . . 10
 
  |
15 | 14 | adantr 471 |
. . . . . . . . 9
 
 
  |
16 | | rspcsbela 3763 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)   |
17 | 12, 15, 16 | syl2anc 671 |
. . . . . . . 8
 
   ![]_ ]_](_urbrack.gif)   |
18 | | eqid 2452 |
. . . . . . . . 9
     |
19 | 18 | fvmpts 5935 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)   |
20 | 12, 17, 19 | syl2anc 671 |
. . . . . . 7
 
         ![]_ ]_](_urbrack.gif)   |
21 | 20 | eqeq1d 2454 |
. . . . . 6
 
        
 ![]_ ]_](_urbrack.gif)
   |
22 | | oveq1 6283 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
23 | | mptscmfsupp0.z |
. . . . . . . . . . . 12
     |
24 | | mptscmfsupp0.r |
. . . . . . . . . . . . . 14
 Scalar    |
25 | 24 | adantr 471 |
. . . . . . . . . . . . 13
 
 Scalar    |
26 | 25 | fveq2d 5852 |
. . . . . . . . . . . 12
 
        Scalar     |
27 | 23, 26 | syl5eq 2498 |
. . . . . . . . . . 11
 
    Scalar     |
28 | 27 | oveq1d 6291 |
. . . . . . . . . 10
 
    ![]_ ]_](_urbrack.gif)      Scalar     ![]_ ]_](_urbrack.gif)    |
29 | | mptscmfsupp0.q |
. . . . . . . . . . . 12
   |
30 | 29 | adantr 471 |
. . . . . . . . . . 11
 
   |
31 | | mptscmfsupp0.w |
. . . . . . . . . . . . . 14
 
   |
32 | 31 | ralrimiva 2790 |
. . . . . . . . . . . . 13
 
  |
33 | 32 | adantr 471 |
. . . . . . . . . . . 12
 
 
  |
34 | | rspcsbela 3763 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif)   |
35 | 12, 33, 34 | syl2anc 671 |
. . . . . . . . . . 11
 
   ![]_ ]_](_urbrack.gif)   |
36 | | mptscmfsupp0.k |
. . . . . . . . . . . 12
     |
37 | | eqid 2452 |
. . . . . . . . . . . 12
Scalar  Scalar   |
38 | | mptscmfsupp0.m |
. . . . . . . . . . . 12
     |
39 | | eqid 2452 |
. . . . . . . . . . . 12
   Scalar      Scalar    |
40 | 36, 37, 38, 39, 6 | lmod0vs 18135 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)      Scalar     ![]_ ]_](_urbrack.gif)   |
41 | 30, 35, 40 | syl2anc 671 |
. . . . . . . . . 10
 
     Scalar     ![]_ ]_](_urbrack.gif)   |
42 | 28, 41 | eqtrd 2486 |
. . . . . . . . 9
 
    ![]_ ]_](_urbrack.gif)   |
43 | 22, 42 | sylan9eqr 2508 |
. . . . . . . 8
      ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
44 | | csbov12g 6312 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
45 | 44 | adantl 472 |
. . . . . . . . . . . . 13
 
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
46 | | ovex 6304 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
47 | 45, 46 | syl6eqel 2538 |
. . . . . . . . . . . 12
 
   ![]_ ]_](_urbrack.gif)     |
48 | | eqid 2452 |
. . . . . . . . . . . . 13
         |
49 | 48 | fvmpts 5935 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif) 
            ![]_ ]_](_urbrack.gif)     |
50 | 12, 47, 49 | syl2anc 671 |
. . . . . . . . . . 11
 
           ![]_ ]_](_urbrack.gif)     |
51 | 50, 45 | eqtrd 2486 |
. . . . . . . . . 10
 
            ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
52 | 51 | eqeq1d 2454 |
. . . . . . . . 9
 
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
53 | 52 | adantr 471 |
. . . . . . . 8
      ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
54 | 43, 53 | mpbird 240 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)           |
55 | 54 | ex 440 |
. . . . . 6
 
  
 ![]_ ]_](_urbrack.gif)
          |
56 | 21, 55 | sylbid 223 |
. . . . 5
 
                  |
57 | 56 | necon3d 2645 |
. . . 4
 
                   |
58 | 57 | ss2rabdv 3478 |
. . 3
         
          |
59 | | ovex 6304 |
. . . . . 6
   |
60 | 59 | rgenw 2749 |
. . . . 5

   |
61 | 48 | fnmpt 5686 |
. . . . 5
 
        |
62 | 60, 61 | mp1i 13 |
. . . 4
       |
63 | | suppvalfn 6909 |
. . . 4
     
      supp

          |
64 | 62, 1, 9, 63 | syl3anc 1271 |
. . 3
      supp

          |
65 | 18 | fnmpt 5686 |
. . . . 5
 
    |
66 | 14, 65 | syl 17 |
. . . 4
     |
67 | | fvex 5858 |
. . . . . 6
     |
68 | 23, 67 | eqeltri 2526 |
. . . . 5
 |
69 | 68 | a1i 11 |
. . . 4
   |
70 | | suppvalfn 6909 |
. . . 4
   
    supp            |
71 | 66, 1, 69, 70 | syl3anc 1271 |
. . 3
    supp            |
72 | 58, 64, 71 | 3sstr4d 3443 |
. 2
      supp    supp    |
73 | | suppssfifsupp 7885 |
. 2
      
         supp 
     supp
   supp        finSupp
 |
74 | 3, 5, 9, 11, 72, 73 | syl32anc 1279 |
1
     finSupp
 |