Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . 3
         |
2 | | eqid 2451 |
. . 3
         |
3 | | lincsum.p |
. . 3
    |
4 | | lmodcmn 18136 |
. . . . 5

CMnd |
5 | 4 | adantr 467 |
. . . 4
        CMnd |
6 | 5 | 3ad2ant1 1029 |
. . 3
           

   finSupp    
finSupp      
CMnd |
7 | | simpr 463 |
. . . 4
               |
8 | 7 | 3ad2ant1 1029 |
. . 3
           

   finSupp    
finSupp      
       |
9 | | simpl 459 |
. . . . . 6
          |
10 | 9 | 3ad2ant1 1029 |
. . . . 5
           

   finSupp    
finSupp      
  |
11 | 10 | adantr 467 |
. . . 4
         
  

   finSupp    
finSupp          |
12 | | elmapi 7493 |
. . . . . . . 8
         |
13 | | ffvelrn 6020 |
. . . . . . . . 9
     
       |
14 | 13 | ex 436 |
. . . . . . . 8
             |
15 | 12, 14 | syl 17 |
. . . . . . 7
           |
16 | 15 | adantr 467 |
. . . . . 6
   
           |
17 | 16 | 3ad2ant2 1030 |
. . . . 5
           

   finSupp    
finSupp      

       |
18 | 17 | imp 431 |
. . . 4
         
  

   finSupp    
finSupp              |
19 | | elelpwi 3962 |
. . . . . . . 8
 
            |
20 | 19 | expcom 437 |
. . . . . . 7
      
       |
21 | 20 | adantl 468 |
. . . . . 6
        
       |
22 | 21 | 3ad2ant1 1029 |
. . . . 5
           

   finSupp    
finSupp      

       |
23 | 22 | imp 431 |
. . . 4
         
  

   finSupp    
finSupp              |
24 | | lincsum.s |
. . . . 5
Scalar   |
25 | | eqid 2451 |
. . . . 5
         |
26 | | lincsum.r |
. . . . 5
     |
27 | 1, 24, 25, 26 | lmodvscl 18108 |
. . . 4
     
                       |
28 | 11, 18, 23, 27 | syl3anc 1268 |
. . 3
         
  

   finSupp    
finSupp                          |
29 | | elmapi 7493 |
. . . . . . . 8
         |
30 | | ffvelrn 6020 |
. . . . . . . . 9
     
       |
31 | 30 | ex 436 |
. . . . . . . 8
             |
32 | 29, 31 | syl 17 |
. . . . . . 7
           |
33 | 32 | adantl 468 |
. . . . . 6
   
           |
34 | 33 | 3ad2ant2 1030 |
. . . . 5
           

   finSupp    
finSupp      

       |
35 | 34 | imp 431 |
. . . 4
         
  

   finSupp    
finSupp              |
36 | 1, 24, 25, 26 | lmodvscl 18108 |
. . . 4
     
                       |
37 | 11, 35, 23, 36 | syl3anc 1268 |
. . 3
         
  

   finSupp    
finSupp                          |
38 | | eqidd 2452 |
. . 3
           

   finSupp    
finSupp      

                             |
39 | | eqidd 2452 |
. . 3
           

   finSupp    
finSupp      

                             |
40 | | id 22 |
. . . 4
        
        |
41 | | simpl 459 |
. . . 4
   
  
    |
42 | | simpl 459 |
. . . 4
  finSupp     finSupp     
finSupp       |
43 | 24, 26 | scmfsupp 40216 |
. . . 4
           finSupp
                   finSupp       |
44 | 40, 41, 42, 43 | syl3an 1310 |
. . 3
           

   finSupp    
finSupp      

             finSupp       |
45 | | simpr 463 |
. . . 4
   
  
    |
46 | | simpr 463 |
. . . 4
  finSupp     finSupp     
finSupp       |
47 | 24, 26 | scmfsupp 40216 |
. . . 4
           finSupp
                   finSupp       |
48 | 40, 45, 46, 47 | syl3an 1310 |
. . 3
           

   finSupp    
finSupp      

             finSupp       |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 17557 |
. 2
           

   finSupp    
finSupp      
 g                                g                
g                   |
50 | 7 | adantr 467 |
. . . . . . 7
           

          |
51 | | elmapfn 7494 |
. . . . . . . 8
     |
52 | 51 | ad2antrl 734 |
. . . . . . 7
           

     |
53 | | elmapfn 7494 |
. . . . . . . 8
     |
54 | 53 | ad2antll 735 |
. . . . . . 7
           

     |
55 | 50, 52, 54 | offvalfv 40177 |
. . . . . 6
           

                    |
56 | 55 | 3adant3 1028 |
. . . . 5
           

   finSupp    
finSupp      
 
               |
57 | 24 | lmodfgrp 18100 |
. . . . . . . . . . 11

  |
58 | | grpmnd 16678 |
. . . . . . . . . . 11
   |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10

  |
60 | 59 | ad3antrrr 736 |
. . . . . . . . 9
         
  

      |
61 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
     
       |
62 | 61 | ex 436 |
. . . . . . . . . . . . 13
             |
63 | 12, 62 | syl 17 |
. . . . . . . . . . . 12
           |
64 | 63 | ad2antrl 734 |
. . . . . . . . . . 11
           

           |
65 | 64 | imp 431 |
. . . . . . . . . 10
         
  

          |
66 | 24 | fveq2i 5868 |
. . . . . . . . . . 11
       Scalar    |
67 | 26, 66 | eqtri 2473 |
. . . . . . . . . 10
   Scalar    |
68 | 65, 67 | syl6eleq 2539 |
. . . . . . . . 9
         
  

           Scalar     |
69 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
     
       |
70 | 69, 67 | syl6eleq 2539 |
. . . . . . . . . . . . 13
     
        Scalar     |
71 | 70 | ex 436 |
. . . . . . . . . . . 12
             Scalar      |
72 | 29, 71 | syl 17 |
. . . . . . . . . . 11
           Scalar      |
73 | 72 | ad2antll 735 |
. . . . . . . . . 10
           

           Scalar      |
74 | 73 | imp 431 |
. . . . . . . . 9
         
  

           Scalar     |
75 | 24 | eqcomi 2460 |
. . . . . . . . . . 11
Scalar   |
76 | 75 | fveq2i 5868 |
. . . . . . . . . 10
   Scalar        |
77 | | lincsum.b |
. . . . . . . . . 10
    |
78 | 76, 77 | mndcl 16545 |
. . . . . . . . 9
         Scalar          Scalar                 Scalar     |
79 | 60, 68, 74, 78 | syl3anc 1268 |
. . . . . . . 8
         
  

        
        Scalar     |
80 | | eqid 2451 |
. . . . . . . 8
                         |
81 | 79, 80 | fmptd 6046 |
. . . . . . 7
           

        
             Scalar     |
82 | | fvex 5875 |
. . . . . . . 8
   Scalar    |
83 | | elmapg 7485 |
. . . . . . . 8
     Scalar  
                       Scalar   

                  Scalar      |
84 | 82, 50, 83 | sylancr 669 |
. . . . . . 7
           

                    Scalar   

                  Scalar      |
85 | 81, 84 | mpbird 236 |
. . . . . 6
           

        
          Scalar  
   |
86 | 85 | 3adant3 1028 |
. . . . 5
           

   finSupp    
finSupp      

               Scalar  
   |
87 | 56, 86 | eqeltrd 2529 |
. . . 4
           

   finSupp    
finSupp      
 
     Scalar  
   |
88 | | lincval 40255 |
. . . 4
         Scalar   
           linC      g                     |
89 | 10, 87, 8, 88 | syl3anc 1268 |
. . 3
           

   finSupp    
finSupp      
     linC      g                     |
90 | 51, 53 | anim12i 570 |
. . . . . . . . . . . 12
   
   
   |
91 | 90 | adantl 468 |
. . . . . . . . . . 11
           

   
   |
92 | 91 | adantr 467 |
. . . . . . . . . 10
         
  

    
   |
93 | 50 | anim1i 572 |
. . . . . . . . . 10
         
  

    
    
   |
94 | | fnfvof 6545 |
. . . . . . . . . 10
  

     
             
       |
95 | 92, 93, 94 | syl2anc 667 |
. . . . . . . . 9
         
  

               
       |
96 | 77 | a1i 11 |
. . . . . . . . . 10
         
  

         |
97 | 96 | oveqd 6307 |
. . . . . . . . 9
         
  

        
                      |
98 | 95, 97 | eqtrd 2485 |
. . . . . . . 8
         
  

                            |
99 | 98 | oveq1d 6305 |
. . . . . . 7
         
  

                                            |
100 | 9 | adantr 467 |
. . . . . . . . 9
           

     |
101 | 100 | adantr 467 |
. . . . . . . 8
         
  

      |
102 | 15 | ad2antrl 734 |
. . . . . . . . 9
           

           |
103 | 102 | imp 431 |
. . . . . . . 8
         
  

          |
104 | 32 | ad2antll 735 |
. . . . . . . . 9
           

           |
105 | 104 | imp 431 |
. . . . . . . 8
         
  

          |
106 | 21 | adantr 467 |
. . . . . . . . 9
           

   
       |
107 | 106 | imp 431 |
. . . . . . . 8
         
  

          |
108 | | eqid 2451 |
. . . . . . . . 9
Scalar  Scalar   |
109 | 24 | fveq2i 5868 |
. . . . . . . . 9
     Scalar    |
110 | 1, 3, 108, 25, 67, 109 | lmodvsdir 18115 |
. . . . . . . 8
                                                                    |
111 | 101, 103,
105, 107, 110 | syl13anc 1270 |
. . . . . . 7
         
  

                                                       |
112 | 99, 111 | eqtrd 2485 |
. . . . . 6
         
  

                                               |
113 | 112 | mpteq2dva 4489 |
. . . . 5
           

                                                  |
114 | 113 | oveq2d 6306 |
. . . 4
           

    g                    g 
                              |
115 | 114 | 3adant3 1028 |
. . 3
           

   finSupp    
finSupp      
 g                    g                                |
116 | 89, 115 | eqtrd 2485 |
. 2
           

   finSupp    
finSupp      
     linC      g                                |
117 | | lincsum.x |
. . . 4
  linC      |
118 | | lincsum.y |
. . . 4
  linC      |
119 | 117, 118 | oveq12i 6302 |
. . 3
     linC       linC       |
120 | 67 | oveq1i 6300 |
. . . . . . . . 9
      Scalar     |
121 | 120 | eleq2i 2521 |
. . . . . . . 8
  
    Scalar      |
122 | 121 | biimpi 198 |
. . . . . . 7
       Scalar      |
123 | 122 | ad2antrl 734 |
. . . . . 6
           

       Scalar      |
124 | | lincval 40255 |
. . . . . 6
      Scalar            linC
     g                  |
125 | 100, 123,
50, 124 | syl3anc 1268 |
. . . . 5
           

     linC
     g                  |
126 | 120 | eleq2i 2521 |
. . . . . . . 8
  
    Scalar      |
127 | 126 | biimpi 198 |
. . . . . . 7
       Scalar      |
128 | 127 | ad2antll 735 |
. . . . . 6
           

       Scalar      |
129 | | lincval 40255 |
. . . . . 6
      Scalar            linC
     g                  |
130 | 100, 128,
50, 129 | syl3anc 1268 |
. . . . 5
           

     linC
     g                  |
131 | 125, 130 | oveq12d 6308 |
. . . 4
           

      linC       linC        g                
g                   |
132 | 131 | 3adant3 1028 |
. . 3
           

   finSupp    
finSupp      
   linC
      linC
       g                 g 
                 |
133 | 119, 132 | syl5eq 2497 |
. 2
           

   finSupp    
finSupp      
    g                
g                   |
134 | 49, 116, 133 | 3eqtr4rd 2496 |
1
           

   finSupp    
finSupp      
       linC       |