Step | Hyp | Ref
| Expression |
1 | | gsumvsca.a |
. 2
   |
2 | | ssid 3437 |
. . 3
 |
3 | | sseq1 3439 |
. . . . . . 7


   |
4 | 3 | anbi2d 718 |
. . . . . 6

 

     |
5 | | mpteq1 4476 |
. . . . . . . 8

          |
6 | 5 | oveq2d 6324 |
. . . . . . 7

 g       g  
     |
7 | | mpteq1 4476 |
. . . . . . . . 9

      |
8 | 7 | oveq2d 6324 |
. . . . . . . 8

 g     g      |
9 | 8 | oveq1d 6323 |
. . . . . . 7

  g       g       |
10 | 6, 9 | eqeq12d 2486 |
. . . . . 6

  g        g      g  
     g        |
11 | 4, 10 | imbi12d 327 |
. . . . 5

     g        g          g  
     g         |
12 | | sseq1 3439 |
. . . . . . 7
 
   |
13 | 12 | anbi2d 718 |
. . . . . 6
  


    |
14 | | mpteq1 4476 |
. . . . . . . 8
           |
15 | 14 | oveq2d 6324 |
. . . . . . 7
  g       g        |
16 | | mpteq1 4476 |
. . . . . . . . 9
       |
17 | 16 | oveq2d 6324 |
. . . . . . . 8
  g     g      |
18 | 17 | oveq1d 6323 |
. . . . . . 7
   g       g       |
19 | 15, 18 | eqeq12d 2486 |
. . . . . 6
   g        g      g        g        |
20 | 13, 19 | imbi12d 327 |
. . . . 5
      g        g       
  g        g         |
21 | | sseq1 3439 |
. . . . . . 7
             |
22 | 21 | anbi2d 718 |
. . . . . 6
      
 
        |
23 | | mpteq1 4476 |
. . . . . . . 8
                   |
24 | 23 | oveq2d 6324 |
. . . . . . 7
      g       g            |
25 | | mpteq1 4476 |
. . . . . . . . 9
               |
26 | 25 | oveq2d 6324 |
. . . . . . . 8
      g     g          |
27 | 26 | oveq1d 6323 |
. . . . . . 7
       g       g           |
28 | 24, 27 | eqeq12d 2486 |
. . . . . 6
       g        g      g            g            |
29 | 22, 28 | imbi12d 327 |
. . . . 5
       
  g        g              g            g             |
30 | | sseq1 3439 |
. . . . . . 7
 
   |
31 | 30 | anbi2d 718 |
. . . . . 6
  


    |
32 | | mpteq1 4476 |
. . . . . . . 8
           |
33 | 32 | oveq2d 6324 |
. . . . . . 7
  g       g        |
34 | | mpteq1 4476 |
. . . . . . . . 9
       |
35 | 34 | oveq2d 6324 |
. . . . . . . 8
  g     g      |
36 | 35 | oveq1d 6323 |
. . . . . . 7
   g       g       |
37 | 33, 36 | eqeq12d 2486 |
. . . . . 6
   g        g      g        g        |
38 | 31, 37 | imbi12d 327 |
. . . . 5
      g        g       
  g        g         |
39 | | gsumvsca.w |
. . . . . . . . 9
 SLMod |
40 | | gsumvsca2.n |
. . . . . . . . 9
   |
41 | | gsumvsca.b |
. . . . . . . . . 10
     |
42 | | gsumvsca.g |
. . . . . . . . . 10
Scalar   |
43 | | gsumvsca.t |
. . . . . . . . . 10
     |
44 | | eqid 2471 |
. . . . . . . . . 10
         |
45 | | gsumvsca.z |
. . . . . . . . . 10
     |
46 | 41, 42, 43, 44, 45 | slmd0vs 28614 |
. . . . . . . . 9
  SLMod
     
  |
47 | 39, 40, 46 | syl2anc 673 |
. . . . . . . 8
        |
48 | 47 | eqcomd 2477 |
. . . . . . 7
         |
49 | | mpt0 5715 |
. . . . . . . . 9
     |
50 | 49 | oveq2i 6319 |
. . . . . . . 8
 g  
    g   |
51 | 45 | gsum0 16599 |
. . . . . . . 8
 g   |
52 | 50, 51 | eqtri 2493 |
. . . . . . 7
 g  
    |
53 | | mpt0 5715 |
. . . . . . . . . 10
   |
54 | 53 | oveq2i 6319 |
. . . . . . . . 9
 g     g   |
55 | 44 | gsum0 16599 |
. . . . . . . . 9
 g       |
56 | 54, 55 | eqtri 2493 |
. . . . . . . 8
 g         |
57 | 56 | oveq1i 6318 |
. . . . . . 7
  g         
  |
58 | 48, 52, 57 | 3eqtr4g 2530 |
. . . . . 6
  g  
     g       |
59 | 58 | adantr 472 |
. . . . 5
 

 g        g       |
60 | | ssun1 3588 |
. . . . . . . . 9
     |
61 | | sstr2 3425 |
. . . . . . . . 9
         
   |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
    
  |
63 | 62 | anim2i 579 |
. . . . . . 7
 
     
   |
64 | 63 | imim1i 59 |
. . . . . 6
     g        g     
        g        g        |
65 | 39 | ad2antrl 742 |
. . . . . . . . . . 11
          
SLMod |
66 | | eqid 2471 |
. . . . . . . . . . . 12
         |
67 | 42 | slmdsrg 28597 |
. . . . . . . . . . . . 13
 SLMod SRing |
68 | | srgcmn 17820 |
. . . . . . . . . . . . 13
 SRing CMnd |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . 12
          
CMnd |
70 | | vex 3034 |
. . . . . . . . . . . . 13
 |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
             |
72 | | simplrl 778 |
. . . . . . . . . . . . . 14
   
        
  |
73 | | simprr 774 |
. . . . . . . . . . . . . . . 16
                 |
74 | 73 | unssad 3602 |
. . . . . . . . . . . . . . 15
          
  |
75 | 74 | sselda 3418 |
. . . . . . . . . . . . . 14
   
        
  |
76 | | gsumvsca.k |
. . . . . . . . . . . . . . . 16

      |
77 | 76 | adantr 472 |
. . . . . . . . . . . . . . 15
 
       |
78 | | gsumvsca2.c |
. . . . . . . . . . . . . . 15
 
   |
79 | 77, 78 | sseldd 3419 |
. . . . . . . . . . . . . 14
 
       |
80 | 72, 75, 79 | syl2anc 673 |
. . . . . . . . . . . . 13
   
        
      |
81 | | eqid 2471 |
. . . . . . . . . . . . 13
     |
82 | 80, 81 | fmptd 6061 |
. . . . . . . . . . . 12
                       |
83 | | simpll 768 |
. . . . . . . . . . . . 13
             |
84 | 72, 75, 78 | syl2anc 673 |
. . . . . . . . . . . . 13
   
        
  |
85 | | fvex 5889 |
. . . . . . . . . . . . . 14
     |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
                 |
87 | 81, 83, 84, 86 | fsuppmptdm 7912 |
. . . . . . . . . . . 12
             finSupp       |
88 | 66, 44, 69, 71, 82, 87 | gsumcl 17627 |
. . . . . . . . . . 11
            g          |
89 | 73 | unssbd 3603 |
. . . . . . . . . . . . 13
               |
90 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
91 | 90 | snss 4087 |
. . . . . . . . . . . . 13

    |
92 | 89, 91 | sylibr 217 |
. . . . . . . . . . . 12
             |
93 | 79 | ralrimiva 2809 |
. . . . . . . . . . . . 13
 
      |
94 | 93 | ad2antrl 742 |
. . . . . . . . . . . 12
           
      |
95 | | rspcsbela 3799 |
. . . . . . . . . . . 12
          ![]_ ]_](_urbrack.gif)       |
96 | 92, 94, 95 | syl2anc 673 |
. . . . . . . . . . 11
           
 ![]_ ]_](_urbrack.gif)
      |
97 | 40 | ad2antrl 742 |
. . . . . . . . . . 11
          
  |
98 | | gsumvsca.p |
. . . . . . . . . . . 12
    |
99 | | eqid 2471 |
. . . . . . . . . . . 12
       |
100 | 41, 98, 42, 43, 66, 99 | slmdvsdir 28606 |
. . . . . . . . . . 11
  SLMod
  g       
  ![]_ ]_](_urbrack.gif)    
     g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
101 | 65, 88, 96, 97, 100 | syl13anc 1294 |
. . . . . . . . . 10
              g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
102 | 101 | adantr 472 |
. . . . . . . . 9
   
         g        g         g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
103 | | nfcsb1v 3365 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
104 | 90 | a1i 11 |
. . . . . . . . . . . 12
             |
105 | | simplr 770 |
. . . . . . . . . . . 12
          
  |
106 | | csbeq1a 3358 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
107 | 103, 66, 99, 69, 83, 80, 104, 105, 96, 106 | gsumunsnf 17669 |
. . . . . . . . . . 11
            g          g           ![]_ ]_](_urbrack.gif)    |
108 | 107 | oveq1d 6323 |
. . . . . . . . . 10
             g            g           ![]_ ]_](_urbrack.gif)     |
109 | 108 | adantr 472 |
. . . . . . . . 9
   
         g        g        g            g           ![]_ ]_](_urbrack.gif)     |
110 | | nfcv 2612 |
. . . . . . . . . . . . 13
  |
111 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
112 | 103, 110,
111 | nfov 6334 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)
  |
113 | | slmdcmn 28595 |
. . . . . . . . . . . . 13
 SLMod CMnd |
114 | 65, 113 | syl 17 |
. . . . . . . . . . . 12
          
CMnd |
115 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
   
        
SLMod |
116 | 72, 40 | syl 17 |
. . . . . . . . . . . . 13
   
        
  |
117 | 41, 42, 43, 66 | slmdvscl 28604 |
. . . . . . . . . . . . 13
  SLMod
   
     |
118 | 115, 80, 116, 117 | syl3anc 1292 |
. . . . . . . . . . . 12
   
        
    |
119 | 41, 42, 43, 66 | slmdvscl 28604 |
. . . . . . . . . . . . 13
  SLMod
  ![]_ ]_](_urbrack.gif)    
  
 ![]_ ]_](_urbrack.gif)
   |
120 | 65, 96, 97, 119 | syl3anc 1292 |
. . . . . . . . . . . 12
              ![]_ ]_](_urbrack.gif)
   |
121 | 106 | oveq1d 6323 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif)    |
122 | 112, 41, 98, 114, 83, 118, 104, 105, 120, 121 | gsumunsnf 17669 |
. . . . . . . . . . 11
            g            g         ![]_ ]_](_urbrack.gif)
    |
123 | 122 | adantr 472 |
. . . . . . . . . 10
   
         g        g       g            g         ![]_ ]_](_urbrack.gif)
    |
124 | | simpr 468 |
. . . . . . . . . . 11
   
         g        g       g        g       |
125 | 124 | oveq1d 6323 |
. . . . . . . . . 10
   
         g        g        g         ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
126 | 123, 125 | eqtrd 2505 |
. . . . . . . . 9
   
         g        g       g             g      
 ![]_ ]_](_urbrack.gif)
    |
127 | 102, 109,
126 | 3eqtr4rd 2516 |
. . . . . . . 8
   
         g        g       g            g           |
128 | 127 | exp31 615 |
. . . . . . 7
 

         g        g      g            g             |
129 | 128 | a2d 28 |
. . . . . 6
 

  
    
 g        g              g            g             |
130 | 64, 129 | syl5 32 |
. . . . 5
 

  
  g        g     
        g            g             |
131 | 11, 20, 29, 38, 59, 130 | findcard2s 7830 |
. . . 4
  
  g        g        |
132 | 131 | imp 436 |
. . 3
      g        g       |
133 | 2, 132 | mpanr2 698 |
. 2
  
 g        g       |
134 | 1, 133 | mpancom 682 |
1
  g        g       |