Step | Hyp | Ref
| Expression |
1 | | dvfcn 21515 |
. . . . . . 7
    
    |
2 | | dvbsss 21509 |
. . . . . . . . 9
   |
3 | | efcl 13485 |
. . . . . . . . . . . . . . . 16
       |
4 | | fconstg 5704 |
. . . . . . . . . . . . . . . 16
                         |
5 | 3, 4 | syl 16 |
. . . . . . . . . . . . . . 15
                     |
6 | 3 | snssd 4125 |
. . . . . . . . . . . . . . 15
      
  |
7 | | fss 5674 |
. . . . . . . . . . . . . . 15
                                         |
8 | 5, 6, 7 | syl2anc 661 |
. . . . . . . . . . . . . 14
               |
9 | | ssid 3482 |
. . . . . . . . . . . . . . 15
 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
   |
11 | | subcl 9719 |
. . . . . . . . . . . . . . . . 17
 
     |
12 | 11 | ancoms 453 |
. . . . . . . . . . . . . . . 16
 
     |
13 | | efcl 13485 |
. . . . . . . . . . . . . . . 16
           |
14 | 12, 13 | syl 16 |
. . . . . . . . . . . . . . 15
 
         |
15 | | eqid 2454 |
. . . . . . . . . . . . . . 15
                 |
16 | 14, 15 | fmptd 5975 |
. . . . . . . . . . . . . 14
               |
17 | | 0cn 9488 |
. . . . . . . . . . . . . . 15
 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
   |
19 | | ax-1cn 9450 |
. . . . . . . . . . . . . . 15
 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
   |
21 | 17 | elexi 3086 |
. . . . . . . . . . . . . . . . . 18
 |
22 | 21 | snid 4012 |
. . . . . . . . . . . . . . . . 17
   |
23 | | opelxpi 4978 |
. . . . . . . . . . . . . . . . 17
 
            |
24 | 22, 23 | mpan2 671 |
. . . . . . . . . . . . . . . 16
          |
25 | | dvconst 21523 |
. . . . . . . . . . . . . . . . 17
                     |
26 | 3, 25 | syl 16 |
. . . . . . . . . . . . . . . 16
                 |
27 | 24, 26 | eleqtrrd 2545 |
. . . . . . . . . . . . . . 15
                |
28 | | df-br 4400 |
. . . . . . . . . . . . . . 15
            
  
            |
29 | 27, 28 | sylibr 212 |
. . . . . . . . . . . . . 14
               |
30 | | eff 13484 |
. . . . . . . . . . . . . . . . . 18
     |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . 17
       |
32 | | eqid 2454 |
. . . . . . . . . . . . . . . . . 18
         |
33 | 12, 32 | fmptd 5975 |
. . . . . . . . . . . . . . . . 17
           |
34 | | oveq1 6206 |
. . . . . . . . . . . . . . . . . . . 20
       |
35 | | ovex 6224 |
. . . . . . . . . . . . . . . . . . . 20
   |
36 | 34, 32, 35 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . . 19
             |
37 | | subid 9738 |
. . . . . . . . . . . . . . . . . . 19
     |
38 | 36, 37 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . 18
           |
39 | | dveflem 21583 |
. . . . . . . . . . . . . . . . . 18
     |
40 | 38, 39 | syl6eqbr 4436 |
. . . . . . . . . . . . . . . . 17
               |
41 | 19 | elexi 3086 |
. . . . . . . . . . . . . . . . . . . . 21
 |
42 | 41 | snid 4012 |
. . . . . . . . . . . . . . . . . . . 20
   |
43 | | opelxpi 4978 |
. . . . . . . . . . . . . . . . . . . 20
 
            |
44 | 42, 43 | mpan2 671 |
. . . . . . . . . . . . . . . . . . 19
          |
45 | | cnelprrecn 9485 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
      |
47 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
48 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
49 | 46 | dvmptid 21563 |
. . . . . . . . . . . . . . . . . . . . 21
         |
50 | | simpl 457 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
51 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
52 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
53 | 46, 52 | dvmptc 21564 |
. . . . . . . . . . . . . . . . . . . . 21
         |
54 | 46, 47, 48, 49, 50, 51, 53 | dvmptsub 21573 |
. . . . . . . . . . . . . . . . . . . 20
             |
55 | | 1m0e1 10542 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
56 | 55 | mpteq2i 4482 |
. . . . . . . . . . . . . . . . . . . . 21
       |
57 | | fconstmpt 4989 |
. . . . . . . . . . . . . . . . . . . . 21
       |
58 | 56, 57 | eqtr4i 2486 |
. . . . . . . . . . . . . . . . . . . 20
         |
59 | 54, 58 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . 19
             |
60 | 44, 59 | eleqtrrd 2545 |
. . . . . . . . . . . . . . . . . 18
            |
61 | | df-br 4400 |
. . . . . . . . . . . . . . . . . 18
                    |
62 | 60, 61 | sylibr 212 |
. . . . . . . . . . . . . . . . 17
           |
63 | | eqid 2454 |
. . . . . . . . . . . . . . . . 17
  ℂfld   ℂfld |
64 | 31, 10, 33, 10, 10, 10, 20, 20, 40, 62, 63 | dvcobr 21552 |
. . . . . . . . . . . . . . . 16
               |
65 | | 1t1e1 10579 |
. . . . . . . . . . . . . . . 16
   |
66 | 64, 65 | syl6breq 4438 |
. . . . . . . . . . . . . . 15
             |
67 | | eqidd 2455 |
. . . . . . . . . . . . . . . . . 18
           |
68 | 31 | feqmptd 5852 |
. . . . . . . . . . . . . . . . . 18
         |
69 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . 18
               |
70 | 12, 67, 68, 69 | fmptco 5984 |
. . . . . . . . . . . . . . . . 17
                 |
71 | 70 | oveq2d 6215 |
. . . . . . . . . . . . . . . 16
                     |
72 | 71 | breqd 4410 |
. . . . . . . . . . . . . . 15
                           |
73 | 66, 72 | mpbid 210 |
. . . . . . . . . . . . . 14
               |
74 | 8, 10, 16, 10, 10, 18, 20, 29, 73, 63 | dvmulbr 21545 |
. . . . . . . . . . . . 13
                                                        |
75 | 16, 52 | ffvelrnd 5952 |
. . . . . . . . . . . . . . . 16
               |
76 | 75 | mul02d 9677 |
. . . . . . . . . . . . . . 15
                 |
77 | | fvex 5808 |
. . . . . . . . . . . . . . . . . 18
     |
78 | 77 | fvconst2 6041 |
. . . . . . . . . . . . . . . . 17
                   |
79 | 78 | oveq2d 6215 |
. . . . . . . . . . . . . . . 16
                       |
80 | 3 | mulid2d 9514 |
. . . . . . . . . . . . . . . 16
             |
81 | 79, 80 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
                     |
82 | 76, 81 | oveq12d 6217 |
. . . . . . . . . . . . . 14
                                       |
83 | 3 | addid2d 9680 |
. . . . . . . . . . . . . 14
             |
84 | 82, 83 | eqtrd 2495 |
. . . . . . . . . . . . 13
                                     |
85 | 74, 84 | breqtrd 4423 |
. . . . . . . . . . . 12
                              |
86 | | cnex 9473 |
. . . . . . . . . . . . . . . . 17
 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
88 | 77 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
       |
89 | | fvex 5808 |
. . . . . . . . . . . . . . . . 17
       |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
         |
91 | | fconstmpt 4989 |
. . . . . . . . . . . . . . . . 17
               |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
                 |
93 | | eqidd 2455 |
. . . . . . . . . . . . . . . 16
                   |
94 | 87, 88, 90, 92, 93 | offval2 6445 |
. . . . . . . . . . . . . . 15
                                    |
95 | 31 | feqmptd 5852 |
. . . . . . . . . . . . . . . 16
         |
96 | | efadd 13496 |
. . . . . . . . . . . . . . . . . . 19
                           |
97 | 50, 12, 96 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
 
                       |
98 | | pncan3 9728 |
. . . . . . . . . . . . . . . . . . 19
 
       |
99 | 98 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . 18
 
               |
100 | 97, 99 | eqtr3d 2497 |
. . . . . . . . . . . . . . . . 17
 
                   |
101 | 100 | mpteq2dva 4485 |
. . . . . . . . . . . . . . . 16
                       |
102 | 95, 101 | eqtr4d 2498 |
. . . . . . . . . . . . . . 15
                 |
103 | 94, 102 | eqtr4d 2498 |
. . . . . . . . . . . . . 14
                      |
104 | 103 | oveq2d 6215 |
. . . . . . . . . . . . 13
                          |
105 | 104 | breqd 4410 |
. . . . . . . . . . . 12
                                        |
106 | 85, 105 | mpbid 210 |
. . . . . . . . . . 11
           |
107 | | vex 3079 |
. . . . . . . . . . . 12
 |
108 | 107, 77 | breldm 5151 |
. . . . . . . . . . 11
        
    |
109 | 106, 108 | syl 16 |
. . . . . . . . . 10
     |
110 | 109 | ssriv 3467 |
. . . . . . . . 9
   |
111 | 2, 110 | eqssi 3479 |
. . . . . . . 8
   |
112 | 111 | feq2i 5659 |
. . . . . . 7
        
        |
113 | 1, 112 | mpbi 208 |
. . . . . 6
       |
114 | 113 | a1i 11 |
. . . . 5
        |
115 | 114 | feqmptd 5852 |
. . . 4
 
          |
116 | | ffun 5668 |
. . . . . . 7
         
   |
117 | 1, 116 | ax-mp 5 |
. . . . . 6
   |
118 | | funbrfv 5838 |
. . . . . 6
           
             |
119 | 117, 106,
118 | mpsyl 63 |
. . . . 5
             |
120 | 119 | mpteq2ia 4481 |
. . . 4
               |
121 | 115, 120 | syl6eq 2511 |
. . 3
 
        |
122 | 30 | a1i 11 |
. . . 4
      |
123 | 122 | feqmptd 5852 |
. . 3
        |
124 | 121, 123 | eqtr4d 2498 |
. 2
 
  |
125 | 124 | trud 1379 |
1
   |