Step | Hyp | Ref
| Expression |
1 | | gsumvsca.a |
. 2
   |
2 | | ssid 3476 |
. . 3
 |
3 | | sseq1 3478 |
. . . . . . 7


   |
4 | 3 | anbi2d 703 |
. . . . . 6

 

     |
5 | | mpteq1 4473 |
. . . . . . . 8

          |
6 | 5 | oveq2d 6209 |
. . . . . . 7

 g       g  
     |
7 | | mpteq1 4473 |
. . . . . . . . 9

      |
8 | 7 | oveq2d 6209 |
. . . . . . . 8

 g     g      |
9 | 8 | oveq1d 6208 |
. . . . . . 7

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

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

     g        g          g  
     g         |
12 | | sseq1 3478 |
. . . . . . 7
 
   |
13 | 12 | anbi2d 703 |
. . . . . 6
  


    |
14 | | mpteq1 4473 |
. . . . . . . 8
           |
15 | 14 | oveq2d 6209 |
. . . . . . 7
  g       g        |
16 | | mpteq1 4473 |
. . . . . . . . 9
       |
17 | 16 | oveq2d 6209 |
. . . . . . . 8
  g     g      |
18 | 17 | oveq1d 6208 |
. . . . . . 7
   g       g       |
19 | 15, 18 | eqeq12d 2473 |
. . . . . 6
   g        g      g        g        |
20 | 13, 19 | imbi12d 320 |
. . . . 5
      g        g       
  g        g         |
21 | | sseq1 3478 |
. . . . . . 7
             |
22 | 21 | anbi2d 703 |
. . . . . 6
      
 
        |
23 | | mpteq1 4473 |
. . . . . . . 8
                   |
24 | 23 | oveq2d 6209 |
. . . . . . 7
      g       g            |
25 | | mpteq1 4473 |
. . . . . . . . 9
               |
26 | 25 | oveq2d 6209 |
. . . . . . . 8
      g     g          |
27 | 26 | oveq1d 6208 |
. . . . . . 7
       g       g           |
28 | 24, 27 | eqeq12d 2473 |
. . . . . 6
       g        g      g            g            |
29 | 22, 28 | imbi12d 320 |
. . . . 5
       
  g        g              g            g             |
30 | | sseq1 3478 |
. . . . . . 7
 
   |
31 | 30 | anbi2d 703 |
. . . . . 6
  


    |
32 | | mpteq1 4473 |
. . . . . . . 8
           |
33 | 32 | oveq2d 6209 |
. . . . . . 7
  g       g        |
34 | | mpteq1 4473 |
. . . . . . . . 9
       |
35 | 34 | oveq2d 6209 |
. . . . . . . 8
  g     g      |
36 | 35 | oveq1d 6208 |
. . . . . . 7
   g       g       |
37 | 33, 36 | eqeq12d 2473 |
. . . . . 6
   g        g      g        g        |
38 | 31, 37 | imbi12d 320 |
. . . . 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 2451 |
. . . . . . . . . 10
         |
45 | | gsumvsca.z |
. . . . . . . . . 10
     |
46 | 41, 42, 43, 44, 45 | slmd0vs 26378 |
. . . . . . . . 9
  SLMod
     
  |
47 | 39, 40, 46 | syl2anc 661 |
. . . . . . . 8
        |
48 | | eqcom 2460 |
. . . . . . . 8
     
       |
49 | 47, 48 | sylibr 212 |
. . . . . . 7
         |
50 | | mpt0 5639 |
. . . . . . . . . 10
     |
51 | 50 | oveq2i 6204 |
. . . . . . . . 9
 g  
    g   |
52 | 45 | gsum0 15621 |
. . . . . . . . 9
 g   |
53 | 51, 52 | eqtri 2480 |
. . . . . . . 8
 g  
    |
54 | | mpt0 5639 |
. . . . . . . . . . 11
   |
55 | 54 | oveq2i 6204 |
. . . . . . . . . 10
 g     g   |
56 | 44 | gsum0 15621 |
. . . . . . . . . 10
 g       |
57 | 55, 56 | eqtri 2480 |
. . . . . . . . 9
 g         |
58 | 57 | oveq1i 6203 |
. . . . . . . 8
  g         
  |
59 | 53, 58 | eqeq12i 2471 |
. . . . . . 7
  g  
     g    
        |
60 | 49, 59 | sylibr 212 |
. . . . . 6
  g  
     g       |
61 | 60 | adantr 465 |
. . . . 5
 

 g        g       |
62 | | ssun1 3620 |
. . . . . . . . 9
     |
63 | | sstr2 3464 |
. . . . . . . . 9
         
   |
64 | 62, 63 | ax-mp 5 |
. . . . . . . 8
    
  |
65 | 64 | anim2i 569 |
. . . . . . 7
 
     
   |
66 | 65 | imim1i 58 |
. . . . . 6
     g        g     
        g        g        |
67 | 39 | ad2antrl 727 |
. . . . . . . . . . . 12
          
SLMod |
68 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
69 | 42 | slmdsrg 26361 |
. . . . . . . . . . . . . 14
 SLMod SRing |
70 | | srgcmn 16724 |
. . . . . . . . . . . . . 14
 SRing CMnd |
71 | 67, 69, 70 | 3syl 20 |
. . . . . . . . . . . . 13
          
CMnd |
72 | | vex 3074 |
. . . . . . . . . . . . . 14
 |
73 | 72 | a1i 11 |
. . . . . . . . . . . . 13
             |
74 | | simplrl 759 |
. . . . . . . . . . . . . . 15
   
        
  |
75 | | simprr 756 |
. . . . . . . . . . . . . . . . 17
                 |
76 | 62, 75 | syl5ss 3468 |
. . . . . . . . . . . . . . . 16
          
  |
77 | 76 | sselda 3457 |
. . . . . . . . . . . . . . 15
   
        
  |
78 | | gsumvsca.k |
. . . . . . . . . . . . . . . . 17

      |
79 | 78 | adantr 465 |
. . . . . . . . . . . . . . . 16
 
       |
80 | | gsumvsca2.c |
. . . . . . . . . . . . . . . 16
 
   |
81 | 79, 80 | sseldd 3458 |
. . . . . . . . . . . . . . 15
 
       |
82 | 74, 77, 81 | syl2anc 661 |
. . . . . . . . . . . . . 14
   
        
      |
83 | | eqid 2451 |
. . . . . . . . . . . . . 14
     |
84 | 82, 83 | fmptd 5969 |
. . . . . . . . . . . . 13
                       |
85 | | simpll 753 |
. . . . . . . . . . . . . 14
             |
86 | 85, 84 | fisuppfi 7732 |
. . . . . . . . . . . . 13
                            |
87 | 68, 44, 71, 73, 84, 86 | gsumclOLD 16513 |
. . . . . . . . . . . 12
            g          |
88 | | ssun2 3621 |
. . . . . . . . . . . . . . 15
 
     |
89 | 88, 75 | syl5ss 3468 |
. . . . . . . . . . . . . 14
               |
90 | | vex 3074 |
. . . . . . . . . . . . . . 15
 |
91 | 90 | snss 4100 |
. . . . . . . . . . . . . 14

    |
92 | 89, 91 | sylibr 212 |
. . . . . . . . . . . . 13
             |
93 | 81 | ralrimiva 2825 |
. . . . . . . . . . . . . 14
 
      |
94 | 93 | ad2antrl 727 |
. . . . . . . . . . . . 13
           
      |
95 | | rspcsbela 3806 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)       |
96 | 92, 94, 95 | syl2anc 661 |
. . . . . . . . . . . 12
           
 ![]_ ]_](_urbrack.gif)
      |
97 | 40 | ad2antrl 727 |
. . . . . . . . . . . 12
          
  |
98 | | gsumvsca.p |
. . . . . . . . . . . . 13
    |
99 | | eqid 2451 |
. . . . . . . . . . . . 13
       |
100 | 41, 98, 42, 43, 68, 99 | slmdvsdir 26370 |
. . . . . . . . . . . 12
  SLMod
  g       
  ![]_ ]_](_urbrack.gif)    
     g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
101 | 67, 87, 96, 97, 100 | syl13anc 1221 |
. . . . . . . . . . 11
              g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
102 | 101 | adantr 465 |
. . . . . . . . . 10
   
         g        g         g           ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
103 | | nfcsb1v 3405 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
104 | 90 | a1i 11 |
. . . . . . . . . . . . 13
             |
105 | | simplr 754 |
. . . . . . . . . . . . 13
          
  |
106 | | csbeq1a 3398 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
107 | 103, 68, 99, 71, 85, 82, 104, 105, 96, 106 | gsumunsnf 26383 |
. . . . . . . . . . . 12
            g          g           ![]_ ]_](_urbrack.gif)    |
108 | 107 | oveq1d 6208 |
. . . . . . . . . . 11
             g            g           ![]_ ]_](_urbrack.gif)     |
109 | 108 | adantr 465 |
. . . . . . . . . 10
   
         g        g        g            g           ![]_ ]_](_urbrack.gif)     |
110 | | nfcv 2613 |
. . . . . . . . . . . . . 14
  |
111 | | nfcv 2613 |
. . . . . . . . . . . . . 14
   |
112 | 103, 110,
111 | nfov 6216 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)
  |
113 | | slmdcmn 26359 |
. . . . . . . . . . . . . 14
 SLMod CMnd |
114 | 67, 113 | syl 16 |
. . . . . . . . . . . . 13
          
CMnd |
115 | 74, 39 | syl 16 |
. . . . . . . . . . . . . 14
   
        
SLMod |
116 | 74, 40 | syl 16 |
. . . . . . . . . . . . . 14
   
        
  |
117 | 41, 42, 43, 68 | slmdvscl 26368 |
. . . . . . . . . . . . . 14
  SLMod
   
     |
118 | 115, 82, 116, 117 | syl3anc 1219 |
. . . . . . . . . . . . 13
   
        
    |
119 | 41, 42, 43, 68 | slmdvscl 26368 |
. . . . . . . . . . . . . 14
  SLMod
  ![]_ ]_](_urbrack.gif)    
  
 ![]_ ]_](_urbrack.gif)
   |
120 | 67, 96, 97, 119 | syl3anc 1219 |
. . . . . . . . . . . . 13
              ![]_ ]_](_urbrack.gif)
   |
121 | 106 | oveq1d 6208 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)    |
122 | 112, 41, 98, 114, 85, 118, 104, 105, 120, 121 | gsumunsnf 26383 |
. . . . . . . . . . . 12
            g            g         ![]_ ]_](_urbrack.gif)
    |
123 | 122 | adantr 465 |
. . . . . . . . . . 11
   
         g        g       g            g         ![]_ ]_](_urbrack.gif)
    |
124 | | simpr 461 |
. . . . . . . . . . . 12
   
         g        g       g        g       |
125 | 124 | oveq1d 6208 |
. . . . . . . . . . 11
   
         g        g        g         ![]_ ]_](_urbrack.gif)      g      
 ![]_ ]_](_urbrack.gif)
    |
126 | 123, 125 | eqtrd 2492 |
. . . . . . . . . 10
   
         g        g       g             g      
 ![]_ ]_](_urbrack.gif)
    |
127 | 102, 109,
126 | 3eqtr4rd 2503 |
. . . . . . . . 9
   
         g        g       g            g           |
128 | 127 | ex 434 |
. . . . . . . 8
             g        g      g            g            |
129 | 128 | ex 434 |
. . . . . . 7
 

         g        g      g            g             |
130 | 129 | a2d 26 |
. . . . . 6
 

  
    
 g        g              g            g             |
131 | 66, 130 | syl5 32 |
. . . . 5
 

  
  g        g     
        g            g             |
132 | 11, 20, 29, 38, 61, 131 | findcard2s 7657 |
. . . 4
  
  g        g        |
133 | 132 | imp 429 |
. . 3
      g        g       |
134 | 2, 133 | mpanr2 684 |
. 2
  
 g        g       |
135 | 1, 134 | mpancom 669 |
1
  g        g       |