Step | Hyp | Ref
| Expression |
1 | | dvmptfprod.i |
. 2
   |
2 | | ssid 3453 |
. . 3
 |
3 | 2 | jctr 545 |
. 2
     |
4 | | sseq1 3455 |
. . . . 5


   |
5 | 4 | anbi2d 711 |
. . . 4

 

     |
6 | | prodeq1 13975 |
. . . . . . 7


   |
7 | 6 | mpteq2dv 4493 |
. . . . . 6

 
      |
8 | 7 | oveq2d 6311 |
. . . . 5

            |
9 | | sumeq1 13767 |
. . . . . . 7


         
         |
10 | | difeq1 3546 |
. . . . . . . . . 10

          |
11 | 10 | prodeq1d 13987 |
. . . . . . . . 9

       
      |
12 | 11 | oveq2d 6311 |
. . . . . . . 8

                  |
13 | 12 | sumeq2sdv 13782 |
. . . . . . 7

          
         |
14 | 9, 13 | eqtrd 2487 |
. . . . . 6


         
         |
15 | 14 | mpteq2dv 4493 |
. . . . 5

 
                      |
16 | 8, 15 | eqeq12d 2468 |
. . . 4

   
   
          

                |
17 | 5, 16 | imbi12d 322 |
. . 3

                                 
          |
18 | | sseq1 3455 |
. . . . 5
 
   |
19 | 18 | anbi2d 711 |
. . . 4
  


    |
20 | | prodeq1 13975 |
. . . . . . 7
  
  |
21 | 20 | mpteq2dv 4493 |
. . . . . 6
     
   |
22 | 21 | oveq2d 6311 |
. . . . 5
             |
23 | | sumeq1 13767 |
. . . . . . 7
 
                   |
24 | | difeq1 3546 |
. . . . . . . . . 10
 
         |
25 | 24 | prodeq1d 13987 |
. . . . . . . . 9
               |
26 | 25 | oveq2d 6311 |
. . . . . . . 8
 
                 |
27 | 26 | sumeq2sdv 13782 |
. . . . . . 7
 
                   |
28 | 23, 27 | eqtrd 2487 |
. . . . . 6
 
                   |
29 | 28 | mpteq2dv 4493 |
. . . . 5
                         |
30 | 22, 29 | eqeq12d 2468 |
. . . 4
                 
  
                |
31 | 19, 30 | imbi12d 322 |
. . 3
                     
  
  
                 |
32 | | sseq1 3455 |
. . . . 5
             |
33 | 32 | anbi2d 711 |
. . . 4
      
 
        |
34 | | prodeq1 13975 |
. . . . . . 7
              |
35 | 34 | mpteq2dv 4493 |
. . . . . 6
                  |
36 | 35 | oveq2d 6311 |
. . . . 5
      

              |
37 | | sumeq1 13767 |
. . . . . . 7
              
               |
38 | | difeq1 3546 |
. . . . . . . . . 10
                   |
39 | 38 | prodeq1d 13987 |
. . . . . . . . 9
           
           |
40 | 39 | oveq2d 6311 |
. . . . . . . 8
                           |
41 | 40 | sumeq2sdv 13782 |
. . . . . . 7
                                       |
42 | 37, 41 | eqtrd 2487 |
. . . . . 6
              
                   |
43 | 42 | mpteq2dv 4493 |
. . . . 5
                                      |
44 | 36, 43 | eqeq12d 2468 |
. . . 4
                     
  
                              |
45 | 33, 44 | imbi12d 322 |
. . 3
       
                                                           |
46 | | sseq1 3455 |
. . . . 5
 
   |
47 | 46 | anbi2d 711 |
. . . 4
  


    |
48 | | prodeq1 13975 |
. . . . . . 7
  
  |
49 | 48 | mpteq2dv 4493 |
. . . . . 6
     
   |
50 | 49 | oveq2d 6311 |
. . . . 5
             |
51 | | sumeq1 13767 |
. . . . . . 7
 
                   |
52 | | difeq1 3546 |
. . . . . . . . . . . 12
 
         |
53 | 52 | prodeq1d 13987 |
. . . . . . . . . . 11
               |
54 | 53 | oveq2d 6311 |
. . . . . . . . . 10
 
                 |
55 | 54 | a1d 26 |
. . . . . . . . 9
                     |
56 | 55 | ralrimiv 2802 |
. . . . . . . 8
 
                  |
57 | 56 | sumeq2d 13780 |
. . . . . . 7
 
                   |
58 | 51, 57 | eqtrd 2487 |
. . . . . 6
 
                   |
59 | 58 | mpteq2dv 4493 |
. . . . 5
                         |
60 | 50, 59 | eqeq12d 2468 |
. . . 4
                 
  
                |
61 | 47, 60 | imbi12d 322 |
. . 3
                     
  
  
                 |
62 | | prod0 14009 |
. . . . . . . 8
  |
63 | 62 | mpteq2i 4489 |
. . . . . . 7
      |
64 | 63 | oveq2i 6306 |
. . . . . 6
          |
65 | 64 | a1i 11 |
. . . . 5
            |
66 | | dvmptfprod.s |
. . . . . 6
      |
67 | | dvmptfprod.x |
. . . . . . 7
   |
68 | | dvmptfprod.j |
. . . . . . . 8

↾t   |
69 | | dvmptfprod.k |
. . . . . . . . 9
  ℂfld |
70 | 69 | oveq1i 6305 |
. . . . . . . 8
 ↾t     ℂfld ↾t   |
71 | 68, 70 | eqtri 2475 |
. . . . . . 7
   ℂfld
↾t   |
72 | 67, 71 | syl6eleq 2541 |
. . . . . 6
    ℂfld ↾t    |
73 | | 1cnd 9664 |
. . . . . 6
   |
74 | 66, 72, 73 | dvmptconst 37795 |
. . . . 5
         |
75 | | sum0 13799 |
. . . . . . . 8
          |
76 | 75 | eqcomi 2462 |
. . . . . . 7
 
        |
77 | 76 | mpteq2i 4489 |
. . . . . 6
    
         |
78 | 77 | a1i 11 |
. . . . 5
       
        |
79 | 65, 74, 78 | 3eqtrd 2491 |
. . . 4
                   |
80 | 79 | adantr 467 |
. . 3
 

  
               |
81 | | simp3 1011 |
. . . . 5
     
                         
       |
82 | | simp1r 1034 |
. . . . 5
     
                        
  |
83 | | simpl 459 |
. . . . . . . . 9
 
       |
84 | | ssun1 3599 |
. . . . . . . . . . 11
     |
85 | | sstr2 3441 |
. . . . . . . . . . 11
         
   |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . 10
    
  |
87 | 86 | adantl 468 |
. . . . . . . . 9
 
    
  |
88 | 83, 87 | jca 535 |
. . . . . . . 8
 
     
   |
89 | 88 | adantl 468 |
. . . . . . 7
                          
 

   |
90 | | simpl 459 |
. . . . . . 7
                          
 
  
  
                |
91 | 89, 90 | mpd 15 |
. . . . . 6
                          
 
  
               |
92 | 91 | 3adant1 1027 |
. . . . 5
     
                                           |
93 | | nfv 1763 |
. . . . . . 7
        
  |
94 | | nfcv 2594 |
. . . . . . . . 9
   |
95 | | nfcv 2594 |
. . . . . . . . 9
  |
96 | | nfmpt1 4495 |
. . . . . . . . 9
   
  |
97 | 94, 95, 96 | nfov 6321 |
. . . . . . . 8
        |
98 | | nfmpt1 4495 |
. . . . . . . 8
              |
99 | 97, 98 | nfeq 2605 |
. . . . . . 7
                   |
100 | 93, 99 | nfan 2013 |
. . . . . 6
         
                   |
101 | | dvmptfprod.iph |
. . . . . . . . 9
   |
102 | | nfv 1763 |
. . . . . . . . 9
       |
103 | 101, 102 | nfan 2013 |
. . . . . . . 8
         |
104 | | nfv 1763 |
. . . . . . . 8
  |
105 | 103, 104 | nfan 2013 |
. . . . . . 7
        
  |
106 | | nfcv 2594 |
. . . . . . . . 9
   |
107 | | nfcv 2594 |
. . . . . . . . 9
  |
108 | | nfcv 2594 |
. . . . . . . . . 10
   |
109 | | nfcv 2594 |
. . . . . . . . . . 11
   |
110 | 109 | nfcprod1 13976 |
. . . . . . . . . 10
    |
111 | 108, 110 | nfmpt 4494 |
. . . . . . . . 9
   
  |
112 | 106, 107,
111 | nfov 6321 |
. . . . . . . 8
        |
113 | | nfcv 2594 |
. . . . . . . . . . 11
   |
114 | | nfcv 2594 |
. . . . . . . . . . 11
  |
115 | | nfcv 2594 |
. . . . . . . . . . . 12
       |
116 | 115 | nfcprod1 13976 |
. . . . . . . . . . 11
         |
117 | 113, 114,
116 | nfov 6321 |
. . . . . . . . . 10
           |
118 | 109, 117 | nfsum 13769 |
. . . . . . . . 9
            |
119 | 108, 118 | nfmpt 4494 |
. . . . . . . 8
              |
120 | 112, 119 | nfeq 2605 |
. . . . . . 7
                   |
121 | 105, 120 | nfan 2013 |
. . . . . 6
         
                   |
122 | | dvmptfprod.jph |
. . . . . . . . 9
   |
123 | | nfv 1763 |
. . . . . . . . 9
       |
124 | 122, 123 | nfan 2013 |
. . . . . . . 8
         |
125 | | nfv 1763 |
. . . . . . . 8
  |
126 | 124, 125 | nfan 2013 |
. . . . . . 7
        
  |
127 | | nfcv 2594 |
. . . . . . . 8
        |
128 | | nfcv 2594 |
. . . . . . . . 9
   |
129 | | nfcv 2594 |
. . . . . . . . . 10
   |
130 | 129 | nfsum1 13768 |
. . . . . . . . 9
            |
131 | 128, 130 | nfmpt 4494 |
. . . . . . . 8
              |
132 | 127, 131 | nfeq 2605 |
. . . . . . 7
                   |
133 | 126, 132 | nfan 2013 |
. . . . . 6
         
                   |
134 | | nfcsb1v 3381 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
135 | | nfcsb1v 3381 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
136 | 83 | ad2antrr 733 |
. . . . . . . 8
        
                    |
137 | 136 | 3ad2ant1 1030 |
. . . . . . 7
         
                 
   |
138 | | simp2 1010 |
. . . . . . 7
         
                 
   |
139 | | simp3 1011 |
. . . . . . 7
         
                 
   |
140 | | dvmptfprod.a |
. . . . . . 7
 

  |
141 | 137, 138,
139, 140 | syl3anc 1269 |
. . . . . 6
         
                 
   |
142 | 136, 1 | syl 17 |
. . . . . . 7
        
                 
  |
143 | 87 | ad2antrr 733 |
. . . . . . 7
        
                 
  |
144 | | ssfi 7797 |
. . . . . . 7
     |
145 | 142, 143,
144 | syl2anc 667 |
. . . . . 6
        
                    |
146 | | vex 3050 |
. . . . . . 7
 |
147 | 146 | a1i 11 |
. . . . . 6
        
                    |
148 | | simplr 763 |
. . . . . 6
        
                 
  |
149 | | simpllr 770 |
. . . . . 6
        
                        |
150 | 66 | ad3antrrr 737 |
. . . . . 6
        
                 
     |
151 | 136 | ad2antrr 733 |
. . . . . . 7
     
    

  
              
   |
152 | 143 | ad2antrr 733 |
. . . . . . . 8
     
    

  
              
   |
153 | | simpr 463 |
. . . . . . . 8
     
    

  
              
   |
154 | 152, 153 | sseldd 3435 |
. . . . . . 7
     
    

  
              
   |
155 | | simplr 763 |
. . . . . . 7
     
    

  
              
   |
156 | | nfv 1763 |
. . . . . . . . . 10
  |
157 | | nfv 1763 |
. . . . . . . . . 10
  |
158 | 101, 156,
157 | nf3an 2015 |
. . . . . . . . 9
  
  |
159 | | nfv 1763 |
. . . . . . . . 9
  |
160 | 158, 159 | nfim 2005 |
. . . . . . . 8
   
   |
161 | | eleq1 2519 |
. . . . . . . . . 10
 
   |
162 | 161 | 3anbi2d 1346 |
. . . . . . . . 9
  


    |
163 | | dvmptfprod.bc |
. . . . . . . . . 10
   |
164 | 163 | eleq1d 2515 |
. . . . . . . . 9
 
   |
165 | 162, 164 | imbi12d 322 |
. . . . . . . 8
   
   
     |
166 | | dvmptfprod.b |
. . . . . . . 8
 

  |
167 | 160, 165,
166 | chvar 2108 |
. . . . . . 7
 

  |
168 | 151, 154,
155, 167 | syl3anc 1269 |
. . . . . 6
     
    

  
              
   |
169 | | simpr 463 |
. . . . . 6
        
                                    |
170 | 83 | adantr 467 |
. . . . . . . . 9
       
   |
171 | | id 22 |
. . . . . . . . . . 11
           |
172 | 146 | snid 3998 |
. . . . . . . . . . . . 13
   |
173 | | elun2 3604 |
. . . . . . . . . . . . 13
         |
174 | 172, 173 | ax-mp 5 |
. . . . . . . . . . . 12
     |
175 | 174 | a1i 11 |
. . . . . . . . . . 11
           |
176 | 171, 175 | sseldd 3435 |
. . . . . . . . . 10
       |
177 | 176 | ad2antlr 734 |
. . . . . . . . 9
       
   |
178 | | simpr 463 |
. . . . . . . . 9
       
   |
179 | | nfv 1763 |
. . . . . . . . . . . 12
  |
180 | | nfv 1763 |
. . . . . . . . . . . 12
  |
181 | 122, 179,
180 | nf3an 2015 |
. . . . . . . . . . 11
  
  |
182 | | nfcv 2594 |
. . . . . . . . . . . 12
   |
183 | 135, 182 | nfel 2606 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
 |
184 | 181, 183 | nfim 2005 |
. . . . . . . . . 10
   
   ![]_ ]_](_urbrack.gif)
  |
185 | | eleq1 2519 |
. . . . . . . . . . . 12
 
   |
186 | 185 | 3anbi2d 1346 |
. . . . . . . . . . 11
  


    |
187 | | csbeq1a 3374 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
188 | 187 | eleq1d 2515 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
189 | 186, 188 | imbi12d 322 |
. . . . . . . . . 10
   
   
   ![]_ ]_](_urbrack.gif)
    |
190 | 184, 189,
167 | chvar 2108 |
. . . . . . . . 9
 

  ![]_ ]_](_urbrack.gif)   |
191 | 170, 177,
178, 190 | syl3anc 1269 |
. . . . . . . 8
       
   ![]_ ]_](_urbrack.gif)   |
192 | 191 | adantlr 722 |
. . . . . . 7
        


  ![]_ ]_](_urbrack.gif)   |
193 | 192 | adantlr 722 |
. . . . . 6
         
                 
   ![]_ ]_](_urbrack.gif)
  |
194 | 122, 179 | nfan 2013 |
. . . . . . . . . 10
     |
195 | | nfcv 2594 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)    |
196 | 128, 135 | nfmpt 4494 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)   |
197 | 195, 196 | nfeq 2605 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
198 | 194, 197 | nfim 2005 |
. . . . . . . . 9
   
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
199 | 185 | anbi2d 711 |
. . . . . . . . . 10
  

     |
200 | | csbeq1a 3374 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
201 | | csbco 3375 |
. . . . . . . . . . . . . . 15
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
203 | 200, 202 | eqtrd 2487 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
204 | 203 | mpteq2dv 4493 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
205 | 204 | oveq2d 6311 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
206 | 187 | mpteq2dv 4493 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)    |
207 | 205, 206 | eqeq12d 2468 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)     |
208 | 199, 207 | imbi12d 322 |
. . . . . . . . 9
   
     ![]_ ]_](_urbrack.gif)     
  
    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)      |
209 | 101, 156 | nfan 2013 |
. . . . . . . . . . 11
     |
210 | | nfcsb1v 3381 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
211 | 108, 210 | nfmpt 4494 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)   |
212 | 106, 107,
211 | nfov 6321 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif)    |
213 | | nfcv 2594 |
. . . . . . . . . . . 12
     |
214 | 212, 213 | nfeq 2605 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)      |
215 | 209, 214 | nfim 2005 |
. . . . . . . . . 10
   
     ![]_ ]_](_urbrack.gif)       |
216 | 161 | anbi2d 711 |
. . . . . . . . . . 11
  

     |
217 | | csbeq1a 3374 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
218 | 217 | mpteq2dv 4493 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)    |
219 | 218 | oveq2d 6311 |
. . . . . . . . . . . 12
      
  ![]_ ]_](_urbrack.gif)     |
220 | 163 | idi 2 |
. . . . . . . . . . . . 13
   |
221 | 220 | mpteq2dv 4493 |
. . . . . . . . . . . 12
       |
222 | 219, 221 | eqeq12d 2468 |
. . . . . . . . . . 11
         
  ![]_ ]_](_urbrack.gif)        |
223 | 216, 222 | imbi12d 322 |
. . . . . . . . . 10
   
       
  
    ![]_ ]_](_urbrack.gif)         |
224 | | dvmptfprod.d |
. . . . . . . . . 10
 
         |
225 | 215, 223,
224 | chvar 2108 |
. . . . . . . . 9
 
     ![]_ ]_](_urbrack.gif)       |
226 | 198, 208,
225 | chvar 2108 |
. . . . . . . 8
 
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
227 | 176, 226 | sylan2 477 |
. . . . . . 7
 
         ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
228 | 227 | ad2antrr 733 |
. . . . . 6
        
                      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
229 | | csbeq1a 3374 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)   |
230 | 100, 121,
133, 134, 135, 141, 145, 147, 148, 149, 150, 168, 169, 193, 228, 229, 187 | dvmptfprodlem 37829 |
. . . . 5
        
                                                  |
231 | 81, 82, 92, 230 | syl21anc 1268 |
. . . 4
     
                                                         |
232 | 231 | 3exp 1208 |
. . 3
 

  
                                                           |
233 | 17, 31, 45, 61, 80, 232 | findcard2s 7817 |
. 2
  
                    |
234 | 1, 3, 233 | sylc 62 |
1
                   |