Proof of Theorem lfl1dim
Step | Hyp | Ref
| Expression |
1 | | df-rab 2746 |
. 2
                       |
2 | | lfl1dim.w |
. . . . . . . . . . . 12
   |
3 | | lveclmod 18329 |
. . . . . . . . . . . 12

  |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
   |
5 | | lfl1dim.d |
. . . . . . . . . . . 12
Scalar   |
6 | | lfl1dim.k |
. . . . . . . . . . . 12
     |
7 | | eqid 2451 |
. . . . . . . . . . . 12
         |
8 | 5, 6, 7 | lmod0cl 18117 |
. . . . . . . . . . 11

      |
9 | 4, 8 | syl 17 |
. . . . . . . . . 10
       |
10 | 9 | ad2antrr 732 |
. . . . . . . . 9
            
      |
11 | | simpr 463 |
. . . . . . . . . 10
            

         |
12 | | lfl1dim.v |
. . . . . . . . . . 11
     |
13 | | lfl1dim.f |
. . . . . . . . . . 11
LFnl   |
14 | | lfl1dim.t |
. . . . . . . . . . 11
     |
15 | 4 | ad2antrr 732 |
. . . . . . . . . . 11
            
  |
16 | | lfl1dim.g |
. . . . . . . . . . . 12
   |
17 | 16 | ad2antrr 732 |
. . . . . . . . . . 11
            
  |
18 | 12, 5, 13, 6, 14, 7, 15, 17 | lfl0sc 32648 |
. . . . . . . . . 10
            
 
                   |
19 | 11, 18 | eqtr4d 2488 |
. . . . . . . . 9
            

            |
20 | | sneq 3978 |
. . . . . . . . . . . . 13
               |
21 | 20 | xpeq2d 4858 |
. . . . . . . . . . . 12
                   |
22 | 21 | oveq2d 6306 |
. . . . . . . . . . 11
              
          |
23 | 22 | eqeq2d 2461 |
. . . . . . . . . 10
            

             |
24 | 23 | rspcev 3150 |
. . . . . . . . 9
     
 
          
 
       |
25 | 10, 19, 24 | syl2anc 667 |
. . . . . . . 8
            


        |
26 | 25 | a1d 26 |
. . . . . . 7
            
        


         |
27 | 9 | ad3antrrr 736 |
. . . . . . . . 9
   

                        |
28 | | lfl1dim.l |
. . . . . . . . . . . . 13
LKer   |
29 | 4 | ad3antrrr 736 |
. . . . . . . . . . . . 13
   

                    |
30 | | simpllr 769 |
. . . . . . . . . . . . 13
   

                    |
31 | 12, 13, 28, 29, 30 | lkrssv 32662 |
. . . . . . . . . . . 12
   

                        |
32 | 4 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   |
33 | 16 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   |
34 | 5, 7, 12, 13, 28 | lkr0f 32660 |
. . . . . . . . . . . . . . . 16
       

          |
35 | 32, 33, 34 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
     

          |
36 | 35 | biimpar 488 |
. . . . . . . . . . . . . 14
            
      |
37 | 36 | sseq1d 3459 |
. . . . . . . . . . . . 13
            
        
       |
38 | 37 | biimpa 487 |
. . . . . . . . . . . 12
   

                        |
39 | 31, 38 | eqssd 3449 |
. . . . . . . . . . 11
   

                        |
40 | 5, 7, 12, 13, 28 | lkr0f 32660 |
. . . . . . . . . . . 12
       

          |
41 | 29, 30, 40 | syl2anc 667 |
. . . . . . . . . . 11
   

                      

          |
42 | 39, 41 | mpbid 214 |
. . . . . . . . . 10
   

                            |
43 | 16 | ad3antrrr 736 |
. . . . . . . . . . 11
   

                    |
44 | 12, 5, 13, 6, 14, 7, 29, 43 | lfl0sc 32648 |
. . . . . . . . . 10
   

                                       |
45 | 42, 44 | eqtr4d 2488 |
. . . . . . . . 9
   

                               |
46 | 27, 45, 24 | syl2anc 667 |
. . . . . . . 8
   

                  

        |
47 | 46 | ex 436 |
. . . . . . 7
            
        


         |
48 | | eqid 2451 |
. . . . . . . . 9
LSHyp  LSHyp   |
49 | 2 | ad2antrr 732 |
. . . . . . . . 9
                      
  |
50 | 16 | ad2antrr 732 |
. . . . . . . . . 10
                      
  |
51 | | simprr 766 |
. . . . . . . . . 10
                      

         |
52 | 12, 5, 7, 48, 13, 28 | lkrshp 32671 |
. . . . . . . . . 10
 
             LSHyp    |
53 | 49, 50, 51, 52 | syl3anc 1268 |
. . . . . . . . 9
                      
    LSHyp    |
54 | | simplr 762 |
. . . . . . . . . 10
                      
  |
55 | | simprl 764 |
. . . . . . . . . 10
                      

         |
56 | 12, 5, 7, 48, 13, 28 | lkrshp 32671 |
. . . . . . . . . 10
 
             LSHyp    |
57 | 49, 54, 55, 56 | syl3anc 1268 |
. . . . . . . . 9
                      
    LSHyp    |
58 | 48, 49, 53, 57 | lshpcmp 32554 |
. . . . . . . 8
                      
                    |
59 | 2 | ad3antrrr 736 |
. . . . . . . . . 10
   
                               |
60 | 16 | ad3antrrr 736 |
. . . . . . . . . 10
   
                               |
61 | | simpllr 769 |
. . . . . . . . . 10
   
                               |
62 | | simpr 463 |
. . . . . . . . . 10
   
                                       |
63 | 5, 6, 14, 12, 13, 28 | eqlkr2 32666 |
. . . . . . . . . 10
  
          
 
       |
64 | 59, 60, 61, 62, 63 | syl121anc 1273 |
. . . . . . . . 9
   
                             

        |
65 | 64 | ex 436 |
. . . . . . . 8
                      
         

         |
66 | 58, 65 | sylbid 219 |
. . . . . . 7
                      
        


         |
67 | 26, 47, 66 | pm2.61da2ne 2712 |
. . . . . 6
 
     
    

         |
68 | 2 | ad2antrr 732 |
. . . . . . . . . 10
       |
69 | 16 | ad2antrr 732 |
. . . . . . . . . 10
       |
70 | | simpr 463 |
. . . . . . . . . 10
       |
71 | 12, 5, 6, 14, 13, 28, 68, 69, 70 | lkrscss 32664 |
. . . . . . . . 9
                      |
72 | 71 | ex 436 |
. . . . . . . 8
 
     
              |
73 | | fveq2 5865 |
. . . . . . . . . 10
       
                 |
74 | 73 | sseq2d 3460 |
. . . . . . . . 9
       
                 
         |
75 | 74 | biimprcd 229 |
. . . . . . . 8
        
      
       
           |
76 | 72, 75 | syl6 34 |
. . . . . . 7
 
     
       
        |
77 | 76 | rexlimdv 2877 |
. . . . . 6
 
  
 
                |
78 | 67, 77 | impbid 194 |
. . . . 5
 
     
   


         |
79 | 78 | pm5.32da 647 |
. . . 4
             

          |
80 | 4 | adantr 467 |
. . . . . . . . 9
 
   |
81 | 16 | adantr 467 |
. . . . . . . . 9
 
   |
82 | | simpr 463 |
. . . . . . . . 9
 
   |
83 | 12, 5, 6, 14, 13, 80, 81, 82 | lflvscl 32643 |
. . . . . . . 8
 
          |
84 | | eleq1a 2524 |
. . . . . . . 8
   
   
       
   |
85 | 83, 84 | syl 17 |
. . . . . . 7
 
            |
86 | 85 | pm4.71rd 641 |
. . . . . 6
 
        

           |
87 | 86 | rexbidva 2898 |
. . . . 5
     
   


           |
88 | | r19.42v 2945 |
. . . . 5
  
 
     



         |
89 | 87, 88 | syl6rbb 266 |
. . . 4
   

       
 
        |
90 | 79, 89 | bitrd 257 |
. . 3
            
 
        |
91 | 90 | abbidv 2569 |
. 2
              
 
        |
92 | 1, 91 | syl5eq 2497 |
1
          
 
 
        |