Step | Hyp | Ref
| Expression |
1 | | simp11 1037 |
. . 3
   

  
finSupp
      
  |
2 | | lincdifsn.s |
. . . . . . . . 9
     |
3 | | lincdifsn.r |
. . . . . . . . . 10
Scalar   |
4 | 3 | fveq2i 5866 |
. . . . . . . . 9
       Scalar    |
5 | 2, 4 | eqtri 2472 |
. . . . . . . 8
   Scalar    |
6 | 5 | oveq1i 6298 |
. . . . . . 7
      Scalar     |
7 | 6 | eleq2i 2520 |
. . . . . 6
  
    Scalar      |
8 | 7 | biimpi 198 |
. . . . 5
       Scalar      |
9 | 8 | adantr 467 |
. . . 4
    finSupp     Scalar      |
10 | 9 | 3ad2ant2 1029 |
. . 3
   

  
finSupp
      
    Scalar      |
11 | | lincdifsn.b |
. . . . . . . 8
     |
12 | 11 | pweqi 3954 |
. . . . . . 7
       |
13 | 12 | eleq2i 2520 |
. . . . . 6
 
       |
14 | 13 | biimpi 198 |
. . . . 5
 
       |
15 | 14 | 3ad2ant2 1029 |
. . . 4
           |
16 | 15 | 3ad2ant1 1028 |
. . 3
   

  
finSupp
      
       |
17 | | lincval 40189 |
. . 3
      Scalar            linC
     g                  |
18 | 1, 10, 16, 17 | syl3anc 1267 |
. 2
   

  
finSupp
      
  linC      g                  |
19 | | lincdifsn.p |
. . . 4
    |
20 | | lmodcmn 18129 |
. . . . . 6

CMnd |
21 | 20 | 3ad2ant1 1028 |
. . . . 5
    CMnd |
22 | 21 | 3ad2ant1 1028 |
. . . 4
   

  
finSupp
      
CMnd |
23 | | simp12 1038 |
. . . 4
   

  
finSupp
      
   |
24 | 14 | anim2i 572 |
. . . . . . 7
             |
25 | 24 | 3adant3 1027 |
. . . . . 6
    
        |
26 | 25 | 3ad2ant1 1028 |
. . . . 5
   

  
finSupp
      

        |
27 | | simp2l 1033 |
. . . . 5
   

  
finSupp
      

   |
28 | | lincdifsn.0 |
. . . . . . . . 9
     |
29 | 28 | breq2i 4409 |
. . . . . . . 8
 finSupp finSupp       |
30 | 29 | biimpi 198 |
. . . . . . 7
 finSupp
finSupp       |
31 | 30 | adantl 468 |
. . . . . 6
    finSupp finSupp       |
32 | 31 | 3ad2ant2 1029 |
. . . . 5
   

  
finSupp
      
finSupp       |
33 | 3, 2 | scmfsupp 40150 |
. . . . 5
           finSupp
                   finSupp       |
34 | 26, 27, 32, 33 | syl3anc 1267 |
. . . 4
   

  
finSupp
      

             finSupp       |
35 | | simpl1 1010 |
. . . . . . 7
   

  
finSupp 
  |
36 | 35 | adantr 467 |
. . . . . 6
     
  
finSupp 
   |
37 | | elmapi 7490 |
. . . . . . . . . 10
         |
38 | | ffvelrn 6018 |
. . . . . . . . . . . 12
     
       |
39 | 38 | ex 436 |
. . . . . . . . . . 11
             |
40 | 39 | a1d 26 |
. . . . . . . . . 10
        

        |
41 | 37, 40 | syl 17 |
. . . . . . . . 9
     


        |
42 | 41 | adantr 467 |
. . . . . . . 8
    finSupp   


        |
43 | 42 | impcom 432 |
. . . . . . 7
   

  
finSupp 

       |
44 | 43 | imp 431 |
. . . . . 6
     
  
finSupp 
       |
45 | | elelpwi 3961 |
. . . . . . . . . 10
 
 
  |
46 | 45 | expcom 437 |
. . . . . . . . 9
      |
47 | 46 | 3ad2ant2 1029 |
. . . . . . . 8
    
   |
48 | 47 | adantr 467 |
. . . . . . 7
   

  
finSupp 

   |
49 | 48 | imp 431 |
. . . . . 6
     
  
finSupp 
   |
50 | | eqid 2450 |
. . . . . . 7
         |
51 | 11, 3, 50, 2 | lmodvscl 18101 |
. . . . . 6
     
               |
52 | 36, 44, 49, 51 | syl3anc 1267 |
. . . . 5
     
  
finSupp 
               |
53 | 52 | 3adantl3 1165 |
. . . 4
     
  
finSupp
                      |
54 | | simp13 1039 |
. . . 4
   

  
finSupp
      
  |
55 | | ffvelrn 6018 |
. . . . . . . . . . 11
     
       |
56 | 55 | expcom 437 |
. . . . . . . . . 10
             |
57 | 56 | 3ad2ant3 1030 |
. . . . . . . . 9
                |
58 | 37, 57 | syl5com 31 |
. . . . . . . 8
     

       |
59 | 58 | adantr 467 |
. . . . . . 7
    finSupp   

       |
60 | 59 | impcom 432 |
. . . . . 6
   

  
finSupp 
      |
61 | | elelpwi 3961 |
. . . . . . . . 9
 
 
  |
62 | 61 | ancoms 455 |
. . . . . . . 8
  

  |
63 | 62 | 3adant1 1025 |
. . . . . . 7
      |
64 | 63 | adantr 467 |
. . . . . 6
   

  
finSupp 
  |
65 | | lincdifsn.t |
. . . . . . 7
     |
66 | 11, 3, 65, 2 | lmodvscl 18101 |
. . . . . 6
     
     
   |
67 | 35, 60, 64, 66 | syl3anc 1267 |
. . . . 5
   

  
finSupp 
        |
68 | 67 | 3adant3 1027 |
. . . 4
   

  
finSupp
      
        |
69 | 65 | eqcomi 2459 |
. . . . . . 7
     |
70 | 69 | a1i 11 |
. . . . . 6
      |
71 | | fveq2 5863 |
. . . . . 6
           |
72 | | id 22 |
. . . . . 6
   |
73 | 70, 71, 72 | oveq123d 6309 |
. . . . 5
                     |
74 | 73 | adantl 468 |
. . . 4
     
  
finSupp
                            |
75 | 11, 19, 22, 23, 34, 53, 54, 68, 74 | gsumdifsnd 17586 |
. . 3
   

  
finSupp
      
 g                  g                             |
76 | | fveq1 5862 |
. . . . . . . . . 10
  
         
          |
77 | 76 | 3ad2ant3 1030 |
. . . . . . . . 9
   

  
finSupp
      
                |
78 | | fvres 5877 |
. . . . . . . . 9
       
             |
79 | 77, 78 | sylan9eq 2504 |
. . . . . . . 8
     
  
finSupp
                      |
80 | 79 | oveq1d 6303 |
. . . . . . 7
     
  
finSupp
                                      |
81 | 80 | mpteq2dva 4488 |
. . . . . 6
   

  
finSupp
      
                                      |
82 | 81 | eqcomd 2456 |
. . . . 5
   

  
finSupp
      
                                      |
83 | 82 | oveq2d 6304 |
. . . 4
   

  
finSupp
      
 g                     g                      |
84 | 83 | oveq1d 6303 |
. . 3
   

  
finSupp
      
  g                             g 
                           |
85 | 75, 84 | eqtrd 2484 |
. 2
   

  
finSupp
      
 g                  g                             |
86 | | eqid 2450 |
. . . . . . . . . . . 12
 |
87 | 86, 5 | feq23i 5720 |
. . . . . . . . . . 11
    
       Scalar     |
88 | 37, 87 | sylib 200 |
. . . . . . . . . 10
          Scalar     |
89 | 88 | adantr 467 |
. . . . . . . . 9
    finSupp        Scalar     |
90 | 89 | 3ad2ant2 1029 |
. . . . . . . 8
   

  
finSupp
      
       Scalar     |
91 | | difssd 3560 |
. . . . . . . 8
   

  
finSupp
      
      |
92 | 90, 91 | fssresd 5748 |
. . . . . . 7
   

  
finSupp
      
                 Scalar     |
93 | | feq1 5708 |
. . . . . . . 8
  
                Scalar    
               Scalar      |
94 | 93 | 3ad2ant3 1030 |
. . . . . . 7
   

  
finSupp
      
            Scalar  
                 Scalar      |
95 | 92, 94 | mpbird 236 |
. . . . . 6
   

  
finSupp
      
           Scalar     |
96 | | fvex 5873 |
. . . . . . 7
   Scalar    |
97 | | difexg 4550 |
. . . . . . . . 9
        |
98 | 97 | 3ad2ant2 1029 |
. . . . . . . 8
          |
99 | 98 | 3ad2ant1 1028 |
. . . . . . 7
   

  
finSupp
      
      |
100 | | elmapg 7482 |
. . . . . . 7
     Scalar  
          Scalar   
   
           Scalar      |
101 | 96, 99, 100 | sylancr 668 |
. . . . . 6
   

  
finSupp
      
     Scalar   
   
           Scalar      |
102 | 95, 101 | mpbird 236 |
. . . . 5
   

  
finSupp
      
    Scalar   
      |
103 | | elpwi 3959 |
. . . . . . . . . 10
    |
104 | 11 | sseq2i 3456 |
. . . . . . . . . . . 12

      |
105 | 104 | biimpi 198 |
. . . . . . . . . . 11
       |
106 | 105 | ssdifssd 3570 |
. . . . . . . . . 10
    
      |
107 | 103, 106 | syl 17 |
. . . . . . . . 9
            |
108 | 107 | adantl 468 |
. . . . . . . 8
              |
109 | 97 | adantl 468 |
. . . . . . . . 9
          |
110 | | elpwg 3958 |
. . . . . . . . 9
                          |
111 | 109, 110 | syl 17 |
. . . . . . . 8
                         |
112 | 108, 111 | mpbird 236 |
. . . . . . 7
               |
113 | 112 | 3adant3 1027 |
. . . . . 6
               |
114 | 113 | 3ad2ant1 1028 |
. . . . 5
   

  
finSupp
      
           |
115 | | lincval 40189 |
. . . . 5
      Scalar   
    
        
  linC          g                      |
116 | 1, 102, 114, 115 | syl3anc 1267 |
. . . 4
   

  
finSupp
      
  linC          g                      |
117 | 116 | eqcomd 2456 |
. . 3
   

  
finSupp
      
 g                      linC           |
118 | 117 | oveq1d 6303 |
. 2
   

  
finSupp
      
  g                              linC                  |
119 | 18, 85, 118 | 3eqtrd 2488 |
1
   

  
finSupp
      
  linC        linC             
    |