Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . . . . 6
ℝ^  ℝ^   |
2 | | eqid 2451 |
. . . . . 6
   ℝ^      ℝ^    |
3 | 1, 2 | rrxds 22352 |
. . . . 5
     ℝ^       ℝ^      RRfld g                       ℝ^     |
4 | | rrxmval.d |
. . . . 5
   ℝ^    |
5 | 3, 4 | syl6reqr 2504 |
. . . 4
     ℝ^       ℝ^      RRfld g                      |
6 | 1, 2 | rrxbase 22347 |
. . . . . 6
    ℝ^      finSupp    |
7 | | rrxmval.1 |
. . . . . 6
   finSupp
  |
8 | 6, 7 | syl6reqr 2504 |
. . . . 5
    ℝ^     |
9 | | mpt2eq12 6351 |
. . . . 5
     ℝ^  
   ℝ^     
   RRfld g                        ℝ^       ℝ^      RRfld g                      |
10 | 8, 8, 9 | syl2anc 667 |
. . . 4
      RRfld g                        ℝ^       ℝ^      RRfld g                      |
11 | 5, 10 | eqtr4d 2488 |
. . 3
      RRfld g                      |
12 | 11 | 3ad2ant1 1029 |
. 2
 
      RRfld g                      |
13 | | simprl 764 |
. . . . . . . . 9
  


    |
14 | 13 | fveq1d 5867 |
. . . . . . . 8
  


            |
15 | | simprr 766 |
. . . . . . . . 9
  


    |
16 | 15 | fveq1d 5867 |
. . . . . . . 8
  


            |
17 | 14, 16 | oveq12d 6308 |
. . . . . . 7
  


                        |
18 | 17 | oveq1d 6305 |
. . . . . 6
  


                                |
19 | 18 | mpteq2dv 4490 |
. . . . 5
  


                                    |
20 | 19 | oveq2d 6306 |
. . . 4
  


  RRfld g                  RRfld g                    |
21 | | simp2 1009 |
. . . . . . . . . . . 12
 
   |
22 | 7, 21 | rrxf 22355 |
. . . . . . . . . . 11
 
       |
23 | 22 | ffvelrnda 6022 |
. . . . . . . . . 10
  

       |
24 | | simp3 1010 |
. . . . . . . . . . . 12
 
   |
25 | 7, 24 | rrxf 22355 |
. . . . . . . . . . 11
 
       |
26 | 25 | ffvelrnda 6022 |
. . . . . . . . . 10
  

       |
27 | 23, 26 | resubcld 10047 |
. . . . . . . . 9
  

             |
28 | 27 | resqcld 12442 |
. . . . . . . 8
  

                 |
29 | | eqid 2451 |
. . . . . . . 8
                                 |
30 | 28, 29 | fmptd 6046 |
. . . . . . 7
 
                       |
31 | 7, 21 | rrxfsupp 22356 |
. . . . . . . . . 10
 
  supp    |
32 | 7, 24 | rrxfsupp 22356 |
. . . . . . . . . 10
 
  supp    |
33 | | unfi 7838 |
. . . . . . . . . 10
   supp   supp     supp   supp     |
34 | 31, 32, 33 | syl2anc 667 |
. . . . . . . . 9
 
   supp   supp     |
35 | 7 | rrxmvallem 22358 |
. . . . . . . . 9
 
                  supp 
  supp   supp     |
36 | | ssfi 7792 |
. . . . . . . . 9
    supp   supp  
                 supp    supp   supp                     supp    |
37 | 34, 35, 36 | syl2anc 667 |
. . . . . . . 8
 
                  supp    |
38 | | mptexg 6135 |
. . . . . . . . . 10
                   |
39 | | funmpt 5618 |
. . . . . . . . . . 11
                 |
40 | | 0cn 9635 |
. . . . . . . . . . 11
 |
41 | | funisfsupp 7888 |
. . . . . . . . . . 11
                  
              
                  finSupp                  supp     |
42 | 39, 40, 41 | mp3an13 1355 |
. . . . . . . . . 10
                                  finSupp
                 supp     |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
                  finSupp
                 supp     |
44 | 43 | 3ad2ant1 1029 |
. . . . . . . 8
 
                  finSupp                  supp     |
45 | 37, 44 | mpbird 236 |
. . . . . . 7
 
                 finSupp   |
46 | | simp1 1008 |
. . . . . . 7
 
   |
47 | | regsumsupp 19190 |
. . . . . . 7
                      
               finSupp  RRfld g                  
                 supp                         |
48 | 30, 45, 46, 47 | syl3anc 1268 |
. . . . . 6
 
 RRfld g                  
                 supp                         |
49 | | suppssdm 6927 |
. . . . . . . . . . 11
                 supp                   |
50 | 29 | dmmptss 5331 |
. . . . . . . . . . 11
               
 |
51 | 49, 50 | sstri 3441 |
. . . . . . . . . 10
                 supp   |
52 | 51 | a1i 11 |
. . . . . . . . 9
 
                  supp 
  |
53 | 52 | sselda 3432 |
. . . . . . . 8
  

                 supp     |
54 | | eqidd 2452 |
. . . . . . . . . 10
  

                                   |
55 | | simpr 463 |
. . . . . . . . . . . . 13
      
  |
56 | 55 | fveq2d 5869 |
. . . . . . . . . . . 12
                 |
57 | 55 | fveq2d 5869 |
. . . . . . . . . . . 12
                 |
58 | 56, 57 | oveq12d 6308 |
. . . . . . . . . . 11
                             |
59 | 58 | oveq1d 6305 |
. . . . . . . . . 10
                                     |
60 | | simpr 463 |
. . . . . . . . . 10
  

   |
61 | | ovex 6318 |
. . . . . . . . . . 11
               |
62 | 61 | a1i 11 |
. . . . . . . . . 10
  

                 |
63 | 54, 59, 60, 62 | fvmptd 5954 |
. . . . . . . . 9
  

                                     |
64 | 63 | eqcomd 2457 |
. . . . . . . 8
  

                                     |
65 | 53, 64 | syldan 473 |
. . . . . . 7
  

                 supp                                       |
66 | 65 | sumeq2dv 13769 |
. . . . . 6
 
                   supp                                   supp                         |
67 | 48, 66 | eqtr4d 2488 |
. . . . 5
 
 RRfld g                  
                 supp                   |
68 | 67 | adantr 467 |
. . . 4
  


  RRfld g                  
                 supp                   |
69 | 22 | ffvelrnda 6022 |
. . . . . . . . . 10
  

       |
70 | 69 | recnd 9669 |
. . . . . . . . 9
  

       |
71 | 25 | ffvelrnda 6022 |
. . . . . . . . . 10
  

       |
72 | 71 | recnd 9669 |
. . . . . . . . 9
  

       |
73 | 70, 72 | subcld 9986 |
. . . . . . . 8
  

             |
74 | 73 | sqcld 12414 |
. . . . . . 7
  

                 |
75 | 53, 74 | syldan 473 |
. . . . . 6
  

                 supp                   |
76 | 7, 21 | rrxsuppss 22357 |
. . . . . . . . . . 11
 
  supp    |
77 | 7, 24 | rrxsuppss 22357 |
. . . . . . . . . . 11
 
  supp    |
78 | 76, 77 | unssd 3610 |
. . . . . . . . . 10
 
   supp   supp     |
79 | 78 | ssdifssd 3571 |
. . . . . . . . 9
 
    supp   supp                    supp     |
80 | 79 | sselda 3432 |
. . . . . . . 8
  

   supp   supp                    supp      |
81 | 80, 64 | syldan 473 |
. . . . . . 7
  

   supp   supp                    supp                                        |
82 | 78 | ssdifd 3569 |
. . . . . . . . 9
 
    supp   supp                    supp   
                 supp     |
83 | 82 | sselda 3432 |
. . . . . . . 8
  

   supp   supp                    supp                      supp     |
84 | | ssid 3451 |
. . . . . . . . . 10
                 supp                   supp   |
85 | 84 | a1i 11 |
. . . . . . . . 9
 
                  supp 
                 supp    |
86 | | 0cnd 9636 |
. . . . . . . . 9
 
   |
87 | 30, 85, 46, 86 | suppssr 6946 |
. . . . . . . 8
  


                 supp   
                      |
88 | 83, 87 | syldan 473 |
. . . . . . 7
  

   supp   supp                    supp                          |
89 | 81, 88 | eqtrd 2485 |
. . . . . 6
  

   supp   supp                    supp                    |
90 | 35, 75, 89, 34 | fsumss 13791 |
. . . . 5
 
                   supp                    supp   supp                    |
91 | 90 | adantr 467 |
. . . 4
  


                    supp                    supp   supp                    |
92 | 20, 68, 91 | 3eqtrd 2489 |
. . 3
  


  RRfld g                     supp   supp                    |
93 | 92 | fveq2d 5869 |
. 2
  


     RRfld g                      
  supp   supp                     |
94 | | fvex 5875 |
. . 3
      supp   supp                    |
95 | 94 | a1i 11 |
. 2
 
    
  supp   supp                     |
96 | 12, 93, 21, 24, 95 | ovmpt2d 6424 |
1
 
           supp   supp                     |