Step | Hyp | Ref
| Expression |
1 | | 3simpa 1027 |
. . . . . . 7
 
 
   |
2 | 1 | ad2antlr 741 |
. . . . . 6
   
  
        |
3 | | fvex 5889 |
. . . . . . . 8
     |
4 | | fvex 5889 |
. . . . . . . 8
          |
5 | 3, 4 | pm3.2i 462 |
. . . . . . 7
                |
6 | 5 | a1i 11 |
. . . . . 6
   
  
        
            |
7 | | simp3 1032 |
. . . . . . 7
 
   |
8 | 7 | ad2antlr 741 |
. . . . . 6
   
  
      |
9 | | fprg 6089 |
. . . . . 6
  

    
                                                          |
10 | 2, 6, 8, 9 | syl3anc 1292 |
. . . . 5
   
  
                             
                     |
11 | | prfi 7864 |
. . . . . 6
    |
12 | 11 | a1i 11 |
. . . . 5
   
  
      
  |
13 | | snlindsntor.0 |
. . . . . . 7
     |
14 | | fvex 5889 |
. . . . . . 7
     |
15 | 13, 14 | eqeltri 2545 |
. . . . . 6
 |
16 | 15 | a1i 11 |
. . . . 5
   
  
   
  |
17 | 10, 12, 16 | fdmfifsupp 7911 |
. . . 4
   
  
                         
finSupp  |
18 | 7 | anim2i 579 |
. . . . . . 7
  
      |
19 | 18 | adantr 472 |
. . . . . 6
   
  
        |
20 | | snlindsntor.r |
. . . . . . . . 9
Scalar   |
21 | | snlindsntor.s |
. . . . . . . . 9
     |
22 | | eqid 2471 |
. . . . . . . . 9
         |
23 | 20, 21, 22 | lmod1cl 18196 |
. . . . . . . 8

      |
24 | | simp1 1030 |
. . . . . . . 8
 

  |
25 | 23, 24 | anim12ci 577 |
. . . . . . 7
  
          |
26 | 25 | adantr 472 |
. . . . . 6
   
  
            |
27 | | simp2 1031 |
. . . . . . 7
 

  |
28 | 27 | ad2antlr 741 |
. . . . . 6
   
  
      |
29 | 20 | lmodfgrp 18178 |
. . . . . . . 8

  |
30 | 29 | adantr 472 |
. . . . . . 7
  
    |
31 | | simpl 464 |
. . . . . . 7
 
  
  |
32 | | eqid 2471 |
. . . . . . . 8
           |
33 | 21, 32 | grpinvcl 16789 |
. . . . . . 7
 
            |
34 | 30, 31, 33 | syl2an 485 |
. . . . . 6
   
  
               |
35 | | snlindsntor.b |
. . . . . . 7
     |
36 | | snlindsntor.t |
. . . . . . 7
     |
37 | | eqid 2471 |
. . . . . . 7
       |
38 | | eqid 2471 |
. . . . . . 7
                     
                       |
39 | 35, 20, 21, 36, 37, 38 | lincvalpr 40719 |
. . . . . 6
          
          
                       linC                             
    |
40 | 19, 26, 28, 34, 39 | syl112anc 1296 |
. . . . 5
   
  
                          
linC                                  |
41 | | simpll 768 |
. . . . . . 7
   
  
      |
42 | 24 | ad2antlr 741 |
. . . . . . . 8
   
  
      |
43 | 31 | adantl 473 |
. . . . . . . 8
   
  
      |
44 | 42, 28, 43 | 3jca 1210 |
. . . . . . 7
   
  
        |
45 | 41, 44 | jca 541 |
. . . . . 6
   
  
          |
46 | | simprr 774 |
. . . . . 6
   
  
        |
47 | | snlindsntor.z |
. . . . . . 7
     |
48 | 35, 20, 21, 13, 47, 36, 22, 32 | ldepsprlem 40773 |
. . . . . 6
  
 
                              |
49 | 45, 46, 48 | sylc 61 |
. . . . 5
   
  
                              |
50 | 40, 49 | eqtrd 2505 |
. . . 4
   
  
                          
linC          |
51 | 20 | lmodring 18177 |
. . . . . . . . . 10

  |
52 | | eqcom 2478 |
. . . . . . . . . . . 12
        
          |
53 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
54 | 21, 53, 22 | 01eq0ring 18573 |
. . . . . . . . . . . . . 14
                   |
55 | | sneq 3969 |
. . . . . . . . . . . . . . . . 17
                       |
56 | 55 | eqeq2d 2481 |
. . . . . . . . . . . . . . . 16
         
               |
57 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . 19
       
         |
58 | | elsni 3985 |
. . . . . . . . . . . . . . . . . . . 20
             |
59 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
60 | 59 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
         |
61 | 27 | anim1i 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  



   |
62 | 61 | ancomd 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  



   |
63 | 35, 20, 36, 22 | lmodvs1 18197 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
   |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  


        |
65 | 64 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  


      
   |
66 | | eqneqall 2654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
67 | 66 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                     |
68 | 67 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                       |
69 | 68 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  



                     |
70 | 65, 69 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


                            |
71 | 70 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       
                       |
72 | 71 | com3r 81 |
. . . . . . . . . . . . . . . . . . . . 21
        


                      |
73 | 60, 72 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . 20
     
   


                       |
74 | 58, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         
 
                         |
75 | 57, 74 | syl6bi 236 |
. . . . . . . . . . . . . . . . . 18
       
    


                        |
76 | 75 | impd 438 |
. . . . . . . . . . . . . . . . 17
               
                       |
77 | 76 | com23 80 |
. . . . . . . . . . . . . . . 16
        
  
                           |
78 | 56, 77 | syl6bi 236 |
. . . . . . . . . . . . . . 15
         
       
  
                            |
79 | 78 | adantl 473 |
. . . . . . . . . . . . . 14
           
       
  
                            |
80 | 54, 79 | mpd 15 |
. . . . . . . . . . . . 13
            

 
                           |
81 | 80 | ex 441 |
. . . . . . . . . . . 12

          

 
                            |
82 | 52, 81 | syl5bi 225 |
. . . . . . . . . . 11

          

 
                            |
83 | 82 | com25 93 |
. . . . . . . . . 10


 
                                       |
84 | 51, 83 | mpcom 36 |
. . . . . . . . 9

 
                                      |
85 | 84 | imp31 439 |
. . . . . . . 8
   
  
            
                     |
86 | | orc 392 |
. . . . . . . 8
                             |
87 | 85, 86 | pm2.61d1 164 |
. . . . . . 7
   
  
                        |
88 | 13 | eqeq2i 2483 |
. . . . . . . . 9
    
          |
89 | 88 | necon3abii 2689 |
. . . . . . . 8
    
          |
90 | 89 | orbi1i 529 |
. . . . . . 7
                                   |
91 | 87, 90 | sylibr 217 |
. . . . . 6
   
  
        
           |
92 | 3 | a1i 11 |
. . . . . . . . 9
   
  
          |
93 | | fvpr1g 6125 |
. . . . . . . . 9
                
                      |
94 | 42, 92, 8, 93 | syl3anc 1292 |
. . . . . . . 8
   
  
                                    |
95 | 94 | neeq1d 2702 |
. . . . . . 7
   
  
                              
      |
96 | 4 | a1i 11 |
. . . . . . . . 9
   
  
               |
97 | | fvpr2g 6126 |
. . . . . . . . 9
                                                 |
98 | 28, 96, 8, 97 | syl3anc 1292 |
. . . . . . . 8
   
  
                                         |
99 | 98 | neeq1d 2702 |
. . . . . . 7
   
  
                              
           |
100 | 95, 99 | orbi12d 724 |
. . . . . 6
   
  
               
                         
                                 |
101 | 91, 100 | mpbird 240 |
. . . . 5
   
  
                                        
                  |
102 | | fveq2 5879 |
. . . . . . . 8
          
                                            |
103 | 102 | neeq1d 2702 |
. . . . . . 7
                           
                            |
104 | | fveq2 5879 |
. . . . . . . 8
          
                                            |
105 | 104 | neeq1d 2702 |
. . . . . . 7
                           
                            |
106 | 103, 105 | rexprg 4013 |
. . . . . 6
 
                                                                    
                   |
107 | 2, 106 | syl 17 |
. . . . 5
   
  
                                                                       
                   |
108 | 101, 107 | mpbird 240 |
. . . 4
   
  
      
                            |
109 | 23 | adantr 472 |
. . . . . . 7
  
        |
110 | 109 | adantr 472 |
. . . . . 6
   
  
          |
111 | | fvex 5889 |
. . . . . . . 8
     |
112 | 21, 111 | eqeltri 2545 |
. . . . . . 7
 |
113 | 8, 112 | jctir 547 |
. . . . . 6
   
  
    
   |
114 | 38 | mapprop 40635 |
. . . . . 6
                              
                    |
115 | 42, 110, 28, 34, 113, 114 | syl221anc 1303 |
. . . . 5
   
  
                                 |
116 | | breq1 4398 |
. . . . . . 7
                        finSupp         
            
finSupp   |
117 | | oveq1 6315 |
. . . . . . . 8
                         linC                 
             linC          |
118 | 117 | eqeq1d 2473 |
. . . . . . 7
                          linC                              
linC           |
119 | | fveq1 5878 |
. . . . . . . . 9
                                                       |
120 | 119 | neeq1d 2702 |
. . . . . . . 8
                           
                            |
121 | 120 | rexbidv 2892 |
. . . . . . 7
                        
         
                             |
122 | 116, 118,
121 | 3anbi123d 1365 |
. . . . . 6
                         finSupp
  linC                                      
finSupp          
             linC                                         |
123 | 122 | adantl 473 |
. . . . 5
       
            
                finSupp   linC                                      
finSupp          
             linC                                         |
124 | 115, 123 | rspcedv 3140 |
. . . 4
   
  
                           
finSupp          
             linC                                         
    finSupp   linC                   |
125 | 17, 50, 108, 124 | mp3and 1393 |
. . 3
   
  
            finSupp
  linC                  |
126 | | prelpwi 4647 |
. . . . . 6
 
   
   |
127 | 126 | 3adant3 1050 |
. . . . 5
 
       |
128 | 127 | ad2antlr 741 |
. . . 4
   
  
      
   |
129 | 35, 47, 20, 21, 13 | islindeps 40754 |
. . . 4
   
      
linDepS
   
    finSupp   linC                   |
130 | 41, 128, 129 | syl2anc 673 |
. . 3
   
  
        linDepS
   
    finSupp   linC                   |
131 | 125, 130 | mpbird 240 |
. 2
   
  
      
linDepS   |
132 | 131 | ex 441 |
1
  
          linDepS    |