Step | Hyp | Ref
| Expression |
1 | | lspsolv.v |
. . 3
     |
2 | | lspsolv.s |
. . 3
     |
3 | | lspsolv.n |
. . 3
     |
4 | | eqid 2461 |
. . 3
Scalar  Scalar   |
5 | | eqid 2461 |
. . 3
   Scalar      Scalar    |
6 | | eqid 2461 |
. . 3
       |
7 | | eqid 2461 |
. . 3
         |
8 | | eqid 2461 |
. . 3
 
   Scalar                         
   Scalar                         |
9 | | lveclmod 18377 |
. . . 4

  |
10 | 9 | adantr 471 |
. . 3
  
    
             |
11 | | simpr1 1020 |
. . 3
  
    
             |
12 | | simpr2 1021 |
. . 3
  
    
             |
13 | | simpr3 1022 |
. . . 4
  
    
               
           |
14 | 13 | eldifad 3427 |
. . 3
  
    
                     |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 14 | lspsolvlem 18413 |
. 2
  
    
               Scalar                         |
16 | 4 | lvecdrng 18376 |
. . . . . . 7

Scalar    |
17 | 16 | ad2antrr 737 |
. . . . . 6
   
    
               Scalar                        Scalar    |
18 | | simprl 769 |
. . . . . 6
   
    
               Scalar                           Scalar     |
19 | 10 | adantr 471 |
. . . . . . . . . . . 12
   
    
               Scalar                       
  |
20 | 12 | adantr 471 |
. . . . . . . . . . . 12
   
    
               Scalar                       
  |
21 | | eqid 2461 |
. . . . . . . . . . . . 13
   Scalar      Scalar    |
22 | | eqid 2461 |
. . . . . . . . . . . . 13
         |
23 | 1, 4, 7, 21, 22 | lmod0vs 18172 |
. . . . . . . . . . . 12
       Scalar                |
24 | 19, 20, 23 | syl2anc 671 |
. . . . . . . . . . 11
   
    
               Scalar                            Scalar                |
25 | 24 | oveq2d 6330 |
. . . . . . . . . 10
   
    
               Scalar                                  Scalar                        |
26 | 11 | adantr 471 |
. . . . . . . . . . . . . . 15
   
    
               Scalar                          |
27 | 20 | snssd 4129 |
. . . . . . . . . . . . . . 15
   
    
               Scalar                            |
28 | 26, 27 | unssd 3621 |
. . . . . . . . . . . . . 14
   
    
               Scalar                              |
29 | 1, 3 | lspssv 18254 |
. . . . . . . . . . . . . 14
  
   
          |
30 | 19, 28, 29 | syl2anc 671 |
. . . . . . . . . . . . 13
   
    
               Scalar                           
      |
31 | 30 | ssdifssd 3582 |
. . . . . . . . . . . 12
   
    
               Scalar                            
           |
32 | 13 | adantr 471 |
. . . . . . . . . . . 12
   
    
               Scalar                       
                |
33 | 31, 32 | sseldd 3444 |
. . . . . . . . . . 11
   
    
               Scalar                       
  |
34 | 1, 6, 22 | lmod0vrid 18170 |
. . . . . . . . . . 11
                |
35 | 19, 33, 34 | syl2anc 671 |
. . . . . . . . . 10
   
    
               Scalar                                     |
36 | 25, 35 | eqtrd 2495 |
. . . . . . . . 9
   
    
               Scalar                                  Scalar             |
37 | 36, 32 | eqeltrd 2539 |
. . . . . . . 8
   
    
               Scalar                                  Scalar               
           |
38 | 37 | eldifbd 3428 |
. . . . . . 7
   
    
               Scalar                                  Scalar                 |
39 | | simprr 771 |
. . . . . . . . 9
   
    
               Scalar                                             |
40 | | oveq1 6321 |
. . . . . . . . . . 11
    Scalar               Scalar            |
41 | 40 | oveq2d 6330 |
. . . . . . . . . 10
    Scalar                            Scalar             |
42 | 41 | eleq1d 2523 |
. . . . . . . . 9
    Scalar                                 Scalar                  |
43 | 39, 42 | syl5ibcom 228 |
. . . . . . . 8
   
    
               Scalar                            Scalar             Scalar                  |
44 | 43 | necon3bd 2649 |
. . . . . . 7
   
    
               Scalar                                   Scalar                  Scalar      |
45 | 38, 44 | mpd 15 |
. . . . . 6
   
    
               Scalar                           Scalar     |
46 | | eqid 2461 |
. . . . . . 7
   Scalar      Scalar    |
47 | | eqid 2461 |
. . . . . . 7
   Scalar      Scalar    |
48 | | eqid 2461 |
. . . . . . 7
   Scalar      Scalar    |
49 | 5, 21, 46, 47, 48 | drnginvrl 18042 |
. . . . . 6
  Scalar 
   Scalar      Scalar         Scalar          Scalar        Scalar     |
50 | 17, 18, 45, 49 | syl3anc 1276 |
. . . . 5
   
    
               Scalar                             Scalar          Scalar        Scalar     |
51 | 50 | oveq1d 6329 |
. . . 4
   
    
               Scalar                              Scalar          Scalar                Scalar            |
52 | 5, 21, 48 | drnginvrcl 18040 |
. . . . . 6
  Scalar 
   Scalar      Scalar        Scalar         Scalar     |
53 | 17, 18, 45, 52 | syl3anc 1276 |
. . . . 5
   
    
               Scalar                            Scalar         Scalar     |
54 | 1, 4, 7, 5, 46 | lmodvsass 18164 |
. . . . 5
       Scalar         Scalar      Scalar  
 
      Scalar          Scalar                 Scalar                       |
55 | 19, 53, 18, 20, 54 | syl13anc 1278 |
. . . 4
   
    
               Scalar                              Scalar          Scalar                 Scalar                       |
56 | 1, 4, 7, 47 | lmodvs1 18167 |
. . . . 5
       Scalar            |
57 | 19, 20, 56 | syl2anc 671 |
. . . 4
   
    
               Scalar                            Scalar            |
58 | 51, 55, 57 | 3eqtr3d 2503 |
. . 3
   
    
               Scalar                             Scalar                       |
59 | 33 | snssd 4129 |
. . . . . 6
   
    
               Scalar                            |
60 | 26, 59 | unssd 3621 |
. . . . 5
   
    
               Scalar                              |
61 | 1, 2, 3 | lspcl 18247 |
. . . . 5
  
   
          |
62 | 19, 60, 61 | syl2anc 671 |
. . . 4
   
    
               Scalar                           
      |
63 | 1, 4, 7, 5 | lmodvscl 18156 |
. . . . . . 7
     Scalar  
           |
64 | 19, 18, 20, 63 | syl3anc 1276 |
. . . . . 6
   
    
               Scalar                                  |
65 | | eqid 2461 |
. . . . . . 7
         |
66 | 1, 6, 65 | lmodvpncan 18189 |
. . . . . 6
                                            |
67 | 19, 64, 33, 66 | syl3anc 1276 |
. . . . 5
   
    
               Scalar                                                         |
68 | 1, 6 | lmodcom 18182 |
. . . . . . . 8
                                           |
69 | 19, 64, 33, 68 | syl3anc 1276 |
. . . . . . 7
   
    
               Scalar                                                        |
70 | | ssun1 3608 |
. . . . . . . . . 10

    |
71 | 70 | a1i 11 |
. . . . . . . . 9
   
    
               Scalar                              |
72 | 1, 3 | lspss 18255 |
. . . . . . . . 9
  
  
            
      |
73 | 19, 60, 71, 72 | syl3anc 1276 |
. . . . . . . 8
   
    
               Scalar                           
          |
74 | 73, 39 | sseldd 3444 |
. . . . . . 7
   
    
               Scalar                                          
      |
75 | 69, 74 | eqeltrd 2539 |
. . . . . 6
   
    
               Scalar                                          
      |
76 | 1, 3 | lspssid 18256 |
. . . . . . . 8
  
   
       
      |
77 | 19, 60, 76 | syl2anc 671 |
. . . . . . 7
   
    
               Scalar                                      |
78 | | snidg 4005 |
. . . . . . . 8
     |
79 | | elun2 3613 |
. . . . . . . 8
         |
80 | 33, 78, 79 | 3syl 18 |
. . . . . . 7
   
    
               Scalar                       
      |
81 | 77, 80 | sseldd 3444 |
. . . . . 6
   
    
               Scalar                       
          |
82 | 65, 2 | lssvsubcl 18215 |
. . . . . 6
      
                        
   
         
                                 |
83 | 19, 62, 75, 81, 82 | syl22anc 1277 |
. . . . 5
   
    
               Scalar                                                  
      |
84 | 67, 83 | eqeltrrd 2540 |
. . . 4
   
    
               Scalar                                          |
85 | 4, 7, 5, 2 | lssvscl 18226 |
. . . 4
      
          Scalar         Scalar              
     
     Scalar                        
      |
86 | 19, 62, 53, 84, 85 | syl22anc 1277 |
. . 3
   
    
               Scalar                             Scalar                        
      |
87 | 58, 86 | eqeltrrd 2540 |
. 2
   
    
               Scalar                       
          |
88 | 15, 87 | rexlimddv 2894 |
1
  
    
                     |