Description: A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pwslnmlem2.a | |
|
pwslnmlem2.b | |
||
pwslnmlem2.x | |
||
pwslnmlem2.y | |
||
pwslnmlem2.z | |
||
pwslnmlem2.w | |
||
pwslnmlem2.dj | |
||
pwslnmlem2.xn | |
||
pwslnmlem2.yn | |
||
Assertion | pwslnmlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwslnmlem2.a | |
|
2 | pwslnmlem2.b | |
|
3 | pwslnmlem2.x | |
|
4 | pwslnmlem2.y | |
|
5 | pwslnmlem2.z | |
|
6 | pwslnmlem2.w | |
|
7 | pwslnmlem2.dj | |
|
8 | pwslnmlem2.xn | |
|
9 | pwslnmlem2.yn | |
|
10 | 1 2 | unex | |
11 | 10 | a1i | |
12 | ssun1 | |
|
13 | 12 | a1i | |
14 | eqid | |
|
15 | eqid | |
|
16 | eqid | |
|
17 | 5 3 14 15 16 | pwssplit3 | |
18 | 6 11 13 17 | syl3anc | |
19 | fvex | |
|
20 | 16 | mptiniseg | |
21 | 19 20 | ax-mp | |
22 | lmodgrp | |
|
23 | grpmnd | |
|
24 | 6 22 23 | 3syl | |
25 | eqid | |
|
26 | 3 25 | pws0g | |
27 | 24 1 26 | sylancl | |
28 | 27 | eqcomd | |
29 | 28 | eqeq2d | |
30 | 29 | rabbidv | |
31 | 21 30 | eqtrid | |
32 | 31 | oveq2d | |
33 | eqid | |
|
34 | eqid | |
|
35 | eqid | |
|
36 | 5 14 25 33 34 3 4 35 | pwssplit4 | |
37 | 6 11 7 36 | syl3anc | |
38 | brlmici | |
|
39 | lnmlmic | |
|
40 | 37 38 39 | 3syl | |
41 | 9 40 | mpbird | |
42 | 32 41 | eqeltrd | |
43 | 5 3 14 15 16 | pwssplit1 | |
44 | 24 11 13 43 | syl3anc | |
45 | forn | |
|
46 | 44 45 | syl | |
47 | 46 | oveq2d | |
48 | 15 | ressid | |
49 | 8 48 | syl | |
50 | 47 49 | eqtrd | |
51 | 50 8 | eqeltrd | |
52 | eqid | |
|
53 | eqid | |
|
54 | eqid | |
|
55 | eqid | |
|
56 | 52 53 54 55 | lmhmlnmsplit | |
57 | 18 42 51 56 | syl3anc | |