Metamath Proof Explorer


Theorem pwslnmlem2

Description: A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypotheses pwslnmlem2.a AV
pwslnmlem2.b BV
pwslnmlem2.x X=W𝑠A
pwslnmlem2.y Y=W𝑠B
pwslnmlem2.z Z=W𝑠AB
pwslnmlem2.w φWLMod
pwslnmlem2.dj φAB=
pwslnmlem2.xn φXLNoeM
pwslnmlem2.yn φYLNoeM
Assertion pwslnmlem2 φZLNoeM

Proof

Step Hyp Ref Expression
1 pwslnmlem2.a AV
2 pwslnmlem2.b BV
3 pwslnmlem2.x X=W𝑠A
4 pwslnmlem2.y Y=W𝑠B
5 pwslnmlem2.z Z=W𝑠AB
6 pwslnmlem2.w φWLMod
7 pwslnmlem2.dj φAB=
8 pwslnmlem2.xn φXLNoeM
9 pwslnmlem2.yn φYLNoeM
10 1 2 unex ABV
11 10 a1i φABV
12 ssun1 AAB
13 12 a1i φAAB
14 eqid BaseZ=BaseZ
15 eqid BaseX=BaseX
16 eqid xBaseZxA=xBaseZxA
17 5 3 14 15 16 pwssplit3 WLModABVAABxBaseZxAZLMHomX
18 6 11 13 17 syl3anc φxBaseZxAZLMHomX
19 fvex 0XV
20 16 mptiniseg 0XVxBaseZxA-10X=xBaseZ|xA=0X
21 19 20 ax-mp xBaseZxA-10X=xBaseZ|xA=0X
22 lmodgrp WLModWGrp
23 grpmnd WGrpWMnd
24 6 22 23 3syl φWMnd
25 eqid 0W=0W
26 3 25 pws0g WMndAVA×0W=0X
27 24 1 26 sylancl φA×0W=0X
28 27 eqcomd φ0X=A×0W
29 28 eqeq2d φxA=0XxA=A×0W
30 29 rabbidv φxBaseZ|xA=0X=xBaseZ|xA=A×0W
31 21 30 eqtrid φxBaseZxA-10X=xBaseZ|xA=A×0W
32 31 oveq2d φZ𝑠xBaseZxA-10X=Z𝑠xBaseZ|xA=A×0W
33 eqid xBaseZ|xA=A×0W=xBaseZ|xA=A×0W
34 eqid yxBaseZ|xA=A×0WyB=yxBaseZ|xA=A×0WyB
35 eqid Z𝑠xBaseZ|xA=A×0W=Z𝑠xBaseZ|xA=A×0W
36 5 14 25 33 34 3 4 35 pwssplit4 WLModABVAB=yxBaseZ|xA=A×0WyBZ𝑠xBaseZ|xA=A×0WLMIsoY
37 6 11 7 36 syl3anc φyxBaseZ|xA=A×0WyBZ𝑠xBaseZ|xA=A×0WLMIsoY
38 brlmici yxBaseZ|xA=A×0WyBZ𝑠xBaseZ|xA=A×0WLMIsoYZ𝑠xBaseZ|xA=A×0W𝑚Y
39 lnmlmic Z𝑠xBaseZ|xA=A×0W𝑚YZ𝑠xBaseZ|xA=A×0WLNoeMYLNoeM
40 37 38 39 3syl φZ𝑠xBaseZ|xA=A×0WLNoeMYLNoeM
41 9 40 mpbird φZ𝑠xBaseZ|xA=A×0WLNoeM
42 32 41 eqeltrd φZ𝑠xBaseZxA-10XLNoeM
43 5 3 14 15 16 pwssplit1 WMndABVAABxBaseZxA:BaseZontoBaseX
44 24 11 13 43 syl3anc φxBaseZxA:BaseZontoBaseX
45 forn xBaseZxA:BaseZontoBaseXranxBaseZxA=BaseX
46 44 45 syl φranxBaseZxA=BaseX
47 46 oveq2d φX𝑠ranxBaseZxA=X𝑠BaseX
48 15 ressid XLNoeMX𝑠BaseX=X
49 8 48 syl φX𝑠BaseX=X
50 47 49 eqtrd φX𝑠ranxBaseZxA=X
51 50 8 eqeltrd φX𝑠ranxBaseZxALNoeM
52 eqid 0X=0X
53 eqid xBaseZxA-10X=xBaseZxA-10X
54 eqid Z𝑠xBaseZxA-10X=Z𝑠xBaseZxA-10X
55 eqid X𝑠ranxBaseZxA=X𝑠ranxBaseZxA
56 52 53 54 55 lmhmlnmsplit xBaseZxAZLMHomXZ𝑠xBaseZxA-10XLNoeMX𝑠ranxBaseZxALNoeMZLNoeM
57 18 42 51 56 syl3anc φZLNoeM