Step | Hyp | Ref
| Expression |
1 | | lcf1o.v |
. . . . . 6
     |
2 | | fvex 5897 |
. . . . . 6
     |
3 | 1, 2 | eqeltri 2535 |
. . . . 5
 |
4 | 3 | mptex 6160 |
. . . 4
   
            |
5 | | lcf1o.j |
. . . 4
      
      
      |
6 | 4, 5 | fnmpti 5727 |
. . 3

  |
7 | 6 | a1i 11 |
. 2
     |
8 | | fvelrnb 5934 |
. . . . 5
    
          |
9 | 7, 8 | syl 17 |
. . . 4
  
          |
10 | | lcf1o.h |
. . . . . . . . 9
     |
11 | | lcf1o.o |
. . . . . . . . 9
         |
12 | | lcf1o.u |
. . . . . . . . 9
         |
13 | | lcf1o.a |
. . . . . . . . 9
    |
14 | | lcf1o.t |
. . . . . . . . 9
     |
15 | | lcf1o.s |
. . . . . . . . 9
Scalar   |
16 | | lcf1o.r |
. . . . . . . . 9
     |
17 | | lcf1o.z |
. . . . . . . . 9
     |
18 | | lcf1o.f |
. . . . . . . . 9
LFnl   |
19 | | lcf1o.l |
. . . . . . . . 9
LKer   |
20 | | lcf1o.d |
. . . . . . . . 9
LDual   |
21 | | lcf1o.q |
. . . . . . . . 9
     |
22 | | lcf1o.c |
. . . . . . . . 9

              |
23 | | lcflo.k |
. . . . . . . . . 10
     |
24 | 23 | adantr 471 |
. . . . . . . . 9
 

  
   |
25 | | simpr 467 |
. . . . . . . . 9
 

      |
26 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 5, 24, 25 | lcfrlem8 35161 |
. . . . . . . 8
 

         
      
      |
27 | | eqid 2461 |
. . . . . . . . . . . 12
   
              
      
     |
28 | | sneq 3989 |
. . . . . . . . . . . . . . . . . 18
       |
29 | 28 | fveq2d 5891 |
. . . . . . . . . . . . . . . . 17
           |
30 | | oveq2 6322 |
. . . . . . . . . . . . . . . . . . 19
 
     |
31 | 30 | oveq2d 6330 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
32 | 31 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . 17
     

      |
33 | 29, 32 | rexeqbidv 3013 |
. . . . . . . . . . . . . . . 16
  
         
            |
34 | 33 | riotabidv 6278 |
. . . . . . . . . . . . . . 15
   
            
      
     |
35 | 34 | mpteq2dv 4503 |
. . . . . . . . . . . . . 14
   

             

             |
36 | 35 | eqeq2d 2471 |
. . . . . . . . . . . . 13
     
             

          

  
              
      
       |
37 | 36 | rspcev 3161 |
. . . . . . . . . . . 12
   

  
              
      
            
      
       
             |
38 | 25, 27, 37 | sylancl 673 |
. . . . . . . . . . 11
 

         
              
      
      |
39 | 38 | olcd 399 |
. . . . . . . . . 10
 

        

                   
              
      
       |
40 | 10, 11, 12, 1, 17, 13, 14, 18, 15, 16, 27, 24, 25 | dochflcl 35087 |
. . . . . . . . . . 11
 

    

             |
41 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 22, 24, 40 | lcfl6 35112 |
. . . . . . . . . 10
 

      
                 

                   
              
      
        |
42 | 39, 41 | mpbird 240 |
. . . . . . . . 9
 

    

             |
43 | 10, 11, 12, 1, 17, 13, 14, 19, 15, 16, 27, 24, 25 | dochsnkr2cl 35086 |
. . . . . . . . . . . 12
 

       
  
                |
44 | 10, 11, 12, 1, 17, 18, 19, 24, 40, 43 | dochsnkrlem3 35083 |
. . . . . . . . . . 11
 

       
  
                   

              |
45 | 10, 11, 12, 1, 17, 18, 19, 24, 40, 43 | dochsnkrlem1 35081 |
. . . . . . . . . . 11
 

       
  
                |
46 | 44, 45 | eqnetrrd 2703 |
. . . . . . . . . 10
 

     
  
              |
47 | 10, 12, 23 | dvhlmod 34722 |
. . . . . . . . . . . . 13
   |
48 | 47 | adantr 471 |
. . . . . . . . . . . 12
 

    |
49 | 1, 18, 19, 20, 21, 48, 40 | lkr0f2 32771 |
. . . . . . . . . . 11
 

        

               
      
       |
50 | 49 | necon3bid 2679 |
. . . . . . . . . 10
 

        

               
      
       |
51 | 46, 50 | mpbid 215 |
. . . . . . . . 9
 

    

             |
52 | | eldifsn 4109 |
. . . . . . . . 9
   

              
   

              
              |
53 | 42, 51, 52 | sylanbrc 675 |
. . . . . . . 8
 

    

                 |
54 | 26, 53 | eqeltrd 2539 |
. . . . . . 7
 

            |
55 | | eleq1 2527 |
. . . . . . 7
                     |
56 | 54, 55 | syl5ibcom 228 |
. . . . . 6
 

              |
57 | 56 | rexlimdva 2890 |
. . . . 5
         

      |
58 | | eldifsn 4109 |
. . . . . . . 8
    

   |
59 | | simprl 769 |
. . . . . . . . 9
 

    |
60 | 47 | adantr 471 |
. . . . . . . . . . . . . 14
 
   |
61 | 22 | lcfl1lem 35103 |
. . . . . . . . . . . . . . . 16


               |
62 | 61 | simplbi 466 |
. . . . . . . . . . . . . . 15
   |
63 | 62 | adantl 472 |
. . . . . . . . . . . . . 14
 
   |
64 | 1, 18, 19, 20, 21, 60, 63 | lkr0f2 32771 |
. . . . . . . . . . . . 13
 
     
   |
65 | 64 | necon3bid 2679 |
. . . . . . . . . . . 12
 
     
   |
66 | 65 | biimprd 231 |
. . . . . . . . . . 11
 
         |
67 | 66 | impr 629 |
. . . . . . . . . 10
 

        |
68 | 67 | neneqd 2639 |
. . . . . . . . 9
 

        |
69 | 23 | adantr 471 |
. . . . . . . . . . . . 13
 

      |
70 | 62 | adantr 471 |
. . . . . . . . . . . . . 14
     |
71 | 70 | adantl 472 |
. . . . . . . . . . . . 13
 

    |
72 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 22, 69, 71 | lcfl6 35112 |
. . . . . . . . . . . 12
 

              

               |
73 | 72 | biimpa 491 |
. . . . . . . . . . 11
      
    
       
              |
74 | 73 | ord 383 |
. . . . . . . . . 10
      
            
              |
75 | 74 | 3impia 1212 |
. . . . . . . . 9
          
       
             |
76 | 59, 68, 75 | mpd3an23 1375 |
. . . . . . . 8
 

  
     

             |
77 | 58, 76 | sylan2b 482 |
. . . . . . 7
 

    
     

             |
78 | | eqcom 2468 |
. . . . . . . . 9
    
      |
79 | 23 | ad2antrr 737 |
. . . . . . . . . . 11
       
  
    |
80 | | simpr 467 |
. . . . . . . . . . 11
       
  

   |
81 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 5, 79, 80 | lcfrlem8 35161 |
. . . . . . . . . 10
       
  
      

             |
82 | 81 | eqeq2d 2471 |
. . . . . . . . 9
       
  
    
   
              |
83 | 78, 82 | syl5bb 265 |
. . . . . . . 8
       
  
    
  

              |
84 | 83 | rexbidva 2909 |
. . . . . . 7
 

                   

              |
85 | 77, 84 | mpbird 240 |
. . . . . 6
 

    
         |
86 | 85 | ex 440 |
. . . . 5
                 |
87 | 57, 86 | impbid 195 |
. . . 4
                 |
88 | 9, 87 | bitrd 261 |
. . 3
         |
89 | 88 | eqrdv 2459 |
. 2
       |
90 | 23 | ad2antrr 737 |
. . . . 5
     

                |
91 | | eqid 2461 |
. . . . 5
   
              
      
     |
92 | | eqid 2461 |
. . . . 5
   
              
      
     |
93 | | simplrl 775 |
. . . . 5
     

                |
94 | | simplrr 776 |
. . . . 5
     

           
    |
95 | | simpr 467 |
. . . . . 6
     

                      |
96 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 5, 90, 93 | lcfrlem8 35161 |
. . . . . 6
     

                   
             |
97 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 5, 90, 94 | lcfrlem8 35161 |
. . . . . 6
     

                   
             |
98 | 95, 96, 97 | 3eqtr3d 2503 |
. . . . 5
     

               
             

             |
99 | 10, 11, 12, 1, 13, 14, 15, 16, 17, 18, 19, 90, 91, 92, 93, 94, 98 | lcfl7lem 35111 |
. . . 4
     

              |
100 | 99 | ex 440 |
. . 3
 
               
   |
101 | 100 | ralrimivva 2820 |
. 2
                     |
102 | | dff1o6 6198 |
. 2
            
                          |
103 | 7, 89, 101, 102 | syl3anbrc 1198 |
1
       
     |