Step | Hyp | Ref
| Expression |
1 | | 3simpa 1005 |
. . . . . . 7
 
 
   |
2 | 1 | ad2antlr 733 |
. . . . . 6
   
  
        |
3 | | fvex 5875 |
. . . . . . . 8
     |
4 | | fvex 5875 |
. . . . . . . 8
          |
5 | 3, 4 | pm3.2i 457 |
. . . . . . 7
                |
6 | 5 | a1i 11 |
. . . . . 6
   
  
        
            |
7 | | simp3 1010 |
. . . . . . 7
 
   |
8 | 7 | ad2antlr 733 |
. . . . . 6
   
  
      |
9 | | fprg 6073 |
. . . . . 6
  

    
                                                          |
10 | 2, 6, 8, 9 | syl3anc 1268 |
. . . . 5
   
  
                             
                     |
11 | | prfi 7846 |
. . . . . 6
    |
12 | 11 | a1i 11 |
. . . . 5
   
  
      
  |
13 | | snlindsntor.0 |
. . . . . . 7
     |
14 | | fvex 5875 |
. . . . . . 7
     |
15 | 13, 14 | eqeltri 2525 |
. . . . . 6
 |
16 | 15 | a1i 11 |
. . . . 5
   
  
   
  |
17 | 10, 12, 16 | fdmfifsupp 7893 |
. . . 4
   
  
                         
finSupp  |
18 | 7 | anim2i 573 |
. . . . . . 7
  
      |
19 | 18 | adantr 467 |
. . . . . 6
   
  
        |
20 | | snlindsntor.r |
. . . . . . . . 9
Scalar   |
21 | | snlindsntor.s |
. . . . . . . . 9
     |
22 | | eqid 2451 |
. . . . . . . . 9
         |
23 | 20, 21, 22 | lmod1cl 18118 |
. . . . . . . 8

      |
24 | | simp1 1008 |
. . . . . . . 8
 

  |
25 | 23, 24 | anim12ci 571 |
. . . . . . 7
  
          |
26 | 25 | adantr 467 |
. . . . . 6
   
  
            |
27 | | simp2 1009 |
. . . . . . 7
 

  |
28 | 27 | ad2antlr 733 |
. . . . . 6
   
  
      |
29 | 20 | lmodfgrp 18100 |
. . . . . . . 8

  |
30 | 29 | adantr 467 |
. . . . . . 7
  
    |
31 | | simpl 459 |
. . . . . . 7
 
  
  |
32 | | eqid 2451 |
. . . . . . . 8
           |
33 | 21, 32 | grpinvcl 16711 |
. . . . . . 7
 
            |
34 | 30, 31, 33 | syl2an 480 |
. . . . . 6
   
  
               |
35 | | snlindsntor.b |
. . . . . . 7
     |
36 | | snlindsntor.t |
. . . . . . 7
     |
37 | | eqid 2451 |
. . . . . . 7
       |
38 | | eqid 2451 |
. . . . . . 7
                     
                       |
39 | 35, 20, 21, 36, 37, 38 | lincvalpr 40264 |
. . . . . 6
          
          
                       linC                             
    |
40 | 19, 26, 28, 34, 39 | syl112anc 1272 |
. . . . 5
   
  
                          
linC                                  |
41 | | simpll 760 |
. . . . . . 7
   
  
      |
42 | 24 | ad2antlr 733 |
. . . . . . . 8
   
  
      |
43 | 31 | adantl 468 |
. . . . . . . 8
   
  
      |
44 | 42, 28, 43 | 3jca 1188 |
. . . . . . 7
   
  
        |
45 | 41, 44 | jca 535 |
. . . . . 6
   
  
          |
46 | | simprr 766 |
. . . . . 6
   
  
        |
47 | | snlindsntor.z |
. . . . . . 7
     |
48 | 35, 20, 21, 13, 47, 36, 22, 32 | ldepsprlem 40318 |
. . . . . 6
  
 
                              |
49 | 45, 46, 48 | sylc 62 |
. . . . 5
   
  
                              |
50 | 40, 49 | eqtrd 2485 |
. . . 4
   
  
                          
linC          |
51 | 20 | lmodring 18099 |
. . . . . . . . . 10

  |
52 | | eqcom 2458 |
. . . . . . . . . . . 12
        
          |
53 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
54 | 21, 53, 22 | 01eq0ring 18496 |
. . . . . . . . . . . . . 14
                   |
55 | | sneq 3978 |
. . . . . . . . . . . . . . . . 17
                       |
56 | 55 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
         
               |
57 | | eleq2 2518 |
. . . . . . . . . . . . . . . . . . 19
       
         |
58 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . 20
             |
59 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
60 | 59 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
         |
61 | 27 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  



   |
62 | 61 | ancomd 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  



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


        |
65 | 64 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  


      
   |
66 | | eqneqall 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
67 | 66 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                     |
68 | 67 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                       |
69 | 68 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  



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


                            |
71 | 70 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       
                       |
72 | 71 | com3r 82 |
. . . . . . . . . . . . . . . . . . . . 21
        


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


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


                        |
76 | 75 | impd 433 |
. . . . . . . . . . . . . . . . 17
               
                       |
77 | 76 | com23 81 |
. . . . . . . . . . . . . . . 16
        
  
                           |
78 | 56, 77 | syl6bi 232 |
. . . . . . . . . . . . . . 15
         
       
  
                            |
79 | 78 | adantl 468 |
. . . . . . . . . . . . . 14
           
       
  
                            |
80 | 54, 79 | mpd 15 |
. . . . . . . . . . . . 13
            

 
                           |
81 | 80 | ex 436 |
. . . . . . . . . . . 12

          

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

          

 
                            |
83 | 82 | com25 94 |
. . . . . . . . . 10


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

 
                                      |
85 | 84 | imp31 434 |
. . . . . . . 8
   
  
            
                     |
86 | | orc 387 |
. . . . . . . 8
                             |
87 | 85, 86 | pm2.61d1 163 |
. . . . . . 7
   
  
                        |
88 | 13 | eqeq2i 2463 |
. . . . . . . . 9
    
          |
89 | 88 | necon3abii 2670 |
. . . . . . . 8
    
          |
90 | 89 | orbi1i 523 |
. . . . . . 7
                                   |
91 | 87, 90 | sylibr 216 |
. . . . . 6
   
  
        
           |
92 | 3 | a1i 11 |
. . . . . . . . 9
   
  
          |
93 | | fvpr1g 6109 |
. . . . . . . . 9
                
                      |
94 | 42, 92, 8, 93 | syl3anc 1268 |
. . . . . . . 8
   
  
                                    |
95 | 94 | neeq1d 2683 |
. . . . . . 7
   
  
                              
      |
96 | 4 | a1i 11 |
. . . . . . . . 9
   
  
               |
97 | | fvpr2g 6110 |
. . . . . . . . 9
                                                 |
98 | 28, 96, 8, 97 | syl3anc 1268 |
. . . . . . . 8
   
  
                                         |
99 | 98 | neeq1d 2683 |
. . . . . . 7
   
  
                              
           |
100 | 95, 99 | orbi12d 716 |
. . . . . 6
   
  
               
                         
                                 |
101 | 91, 100 | mpbird 236 |
. . . . 5
   
  
                                        
                  |
102 | | fveq2 5865 |
. . . . . . . 8
          
                                            |
103 | 102 | neeq1d 2683 |
. . . . . . 7
                           
                            |
104 | | fveq2 5865 |
. . . . . . . 8
          
                                            |
105 | 104 | neeq1d 2683 |
. . . . . . 7
                           
                            |
106 | 103, 105 | rexprg 4022 |
. . . . . 6
 
                                                                    
                   |
107 | 2, 106 | syl 17 |
. . . . 5
   
  
                                                                       
                   |
108 | 101, 107 | mpbird 236 |
. . . 4
   
  
      
                            |
109 | 23 | adantr 467 |
. . . . . . 7
  
        |
110 | 109 | adantr 467 |
. . . . . 6
   
  
          |
111 | | fvex 5875 |
. . . . . . . 8
     |
112 | 21, 111 | eqeltri 2525 |
. . . . . . 7
 |
113 | 8, 112 | jctir 541 |
. . . . . 6
   
  
    
   |
114 | 38 | mapprop 40180 |
. . . . . 6
                              
                    |
115 | 42, 110, 28, 34, 113, 114 | syl221anc 1279 |
. . . . 5
   
  
                                 |
116 | | breq1 4405 |
. . . . . . 7
                        finSupp         
            
finSupp   |
117 | | oveq1 6297 |
. . . . . . . 8
                         linC                 
             linC          |
118 | 117 | eqeq1d 2453 |
. . . . . . 7
                          linC                              
linC           |
119 | | fveq1 5864 |
. . . . . . . . 9
                                                       |
120 | 119 | neeq1d 2683 |
. . . . . . . 8
                           
                            |
121 | 120 | rexbidv 2901 |
. . . . . . 7
                        
         
                             |
122 | 116, 118,
121 | 3anbi123d 1339 |
. . . . . 6
                         finSupp
  linC                                      
finSupp          
             linC                                         |
123 | 122 | adantl 468 |
. . . . 5
       
            
                finSupp   linC                                      
finSupp          
             linC                                         |
124 | 115, 123 | rspcedv 3154 |
. . . 4
   
  
                           
finSupp          
             linC                                         
    finSupp   linC                   |
125 | 17, 50, 108, 124 | mp3and 1367 |
. . 3
   
  
            finSupp
  linC                  |
126 | | prelpwi 4647 |
. . . . . 6
 
   
   |
127 | 126 | 3adant3 1028 |
. . . . 5
 
       |
128 | 127 | ad2antlr 733 |
. . . 4
   
  
      
   |
129 | 35, 47, 20, 21, 13 | islindeps 40299 |
. . . 4
   
      
linDepS
   
    finSupp   linC                   |
130 | 41, 128, 129 | syl2anc 667 |
. . 3
   
  
        linDepS
   
    finSupp   linC                   |
131 | 125, 130 | mpbird 236 |
. 2
   
  
      
linDepS   |
132 | 131 | ex 436 |
1
  
          linDepS    |