Proof of Theorem frlmgsum
Step | Hyp | Ref
| Expression |
1 | | frlmgsum.r |
. . . 4
   |
2 | | frlmgsum.i |
. . . 4
   |
3 | | frlmgsum.y |
. . . . 5
 freeLMod
  |
4 | | frlmgsum.b |
. . . . 5
     |
5 | 3, 4 | frlmpws 19306 |
. . . 4
     ringLMod  s  ↾s    |
6 | 1, 2, 5 | syl2anc 666 |
. . 3
   ringLMod  s 
↾s    |
7 | 6 | oveq1d 6303 |
. 2
  g         ringLMod  s 
↾s  g        |
8 | | eqid 2450 |
. . 3
    ringLMod  s       ringLMod  s    |
9 | | eqid 2450 |
. . 3
   ringLMod  s      ringLMod  s    |
10 | | eqid 2450 |
. . 3
  ringLMod  s 
↾s    ringLMod  s 
↾s   |
11 | | ovex 6316 |
. . . 4
 ringLMod  s   |
12 | 11 | a1i 11 |
. . 3
  ringLMod  s    |
13 | | frlmgsum.j |
. . 3
   |
14 | | eqid 2450 |
. . . . . 6
    ringLMod  s       ringLMod  s    |
15 | 3, 4, 14 | frlmlss 19307 |
. . . . 5
       ringLMod  s     |
16 | 1, 2, 15 | syl2anc 666 |
. . . 4
     ringLMod  s     |
17 | 8, 14 | lssss 18153 |
. . . 4
     ringLMod  s       ringLMod  s     |
18 | 16, 17 | syl 17 |
. . 3

    ringLMod  s     |
19 | | frlmgsum.f |
. . . 4
 
     |
20 | | eqid 2450 |
. . . 4
         |
21 | 19, 20 | fmptd 6044 |
. . 3
           |
22 | | rlmlmod 18421 |
. . . . . 6

ringLMod    |
23 | 1, 22 | syl 17 |
. . . . 5
 ringLMod    |
24 | | eqid 2450 |
. . . . . 6
 ringLMod  s   ringLMod  s   |
25 | 24 | pwslmod 18186 |
. . . . 5
  ringLMod 
  ringLMod  s    |
26 | 23, 2, 25 | syl2anc 666 |
. . . 4
  ringLMod  s    |
27 | | eqid 2450 |
. . . . 5
    ringLMod  s       ringLMod  s    |
28 | 27, 14 | lss0cl 18163 |
. . . 4
   ringLMod  s      ringLMod  s        ringLMod  s     |
29 | 26, 16, 28 | syl2anc 666 |
. . 3
     ringLMod  s     |
30 | | lmodcmn 18129 |
. . . . . . 7
 ringLMod  ringLMod  CMnd |
31 | 23, 30 | syl 17 |
. . . . . 6
 ringLMod  CMnd |
32 | | cmnmnd 17438 |
. . . . . 6
 ringLMod  CMnd ringLMod    |
33 | 31, 32 | syl 17 |
. . . . 5
 ringLMod    |
34 | 24 | pwsmnd 16564 |
. . . . 5
  ringLMod    ringLMod  s    |
35 | 33, 2, 34 | syl2anc 666 |
. . . 4
  ringLMod  s    |
36 | 8, 9, 27 | mndlrid 16549 |
. . . 4
   ringLMod  s      ringLMod  s          ringLMod  s       ringLMod  s          ringLMod  s        ringLMod  s       |
37 | 35, 36 | sylan 474 |
. . 3
 
    ringLMod  s          ringLMod  s       ringLMod  s          ringLMod  s        ringLMod  s       |
38 | 8, 9, 10, 12, 13, 18, 21, 29, 37 | gsumress 16512 |
. 2
   ringLMod  s  g         ringLMod  s 
↾s  g        |
39 | | rlmbas 18411 |
. . . 4
       ringLMod    |
40 | 2 | adantr 467 |
. . . . . . . . 9
 
   |
41 | | eqid 2450 |
. . . . . . . . . 10
         |
42 | 3, 41, 4 | frlmbasf 19316 |
. . . . . . . . 9
  
 

           |
43 | 40, 19, 42 | syl2anc 666 |
. . . . . . . 8
 
             |
44 | | eqid 2450 |
. . . . . . . . 9
     |
45 | 44 | fmpt 6041 |
. . . . . . . 8
 
                |
46 | 43, 45 | sylibr 216 |
. . . . . . 7
 
 
      |
47 | 46 | r19.21bi 2756 |
. . . . . 6
           |
48 | 47 | an32s 812 |
. . . . 5
           |
49 | 48 | anasss 652 |
. . . 4
 

 
      |
50 | | frlmgsum.w |
. . . . 5
     finSupp  |
51 | | frlmgsum.z |
. . . . . 6
     |
52 | 6 | fveq2d 5867 |
. . . . . . 7
          ringLMod  s  ↾s     |
53 | 14 | lsssubg 18173 |
. . . . . . . . 9
   ringLMod  s      ringLMod  s    SubGrp  ringLMod  s     |
54 | 26, 16, 53 | syl2anc 666 |
. . . . . . . 8
 SubGrp  ringLMod  s     |
55 | 10, 27 | subg0 16816 |
. . . . . . . 8
 SubGrp  ringLMod  s       ringLMod  s        ringLMod  s 
↾s     |
56 | 54, 55 | syl 17 |
. . . . . . 7
     ringLMod  s        ringLMod  s 
↾s     |
57 | 52, 56 | eqtr4d 2487 |
. . . . . 6
         ringLMod  s     |
58 | 51, 57 | syl5eq 2496 |
. . . . 5
     ringLMod  s     |
59 | 50, 58 | breqtrd 4426 |
. . . 4
     finSupp     ringLMod  s     |
60 | 24, 39, 27, 2, 13, 31, 49, 59 | pwsgsum 17604 |
. . 3
   ringLMod  s  g        ringLMod  g       |
61 | | mptexg 6133 |
. . . . . 6
     |
62 | 13, 61 | syl 17 |
. . . . 5
     |
63 | | fvex 5873 |
. . . . . 6
ringLMod   |
64 | 63 | a1i 11 |
. . . . 5
 ringLMod    |
65 | 39 | a1i 11 |
. . . . 5
        ringLMod     |
66 | | rlmplusg 18412 |
. . . . . 6
     ringLMod    |
67 | 66 | a1i 11 |
. . . . 5
      ringLMod     |
68 | 62, 1, 64, 65, 67 | gsumpropd 16508 |
. . . 4
  g     ringLMod  g      |
69 | 68 | mpteq2dv 4489 |
. . 3
   g       ringLMod  g       |
70 | 60, 69 | eqtr4d 2487 |
. 2
   ringLMod  s  g        g       |
71 | 7, 38, 70 | 3eqtr2d 2490 |
1
  g        g       |