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 ⊢ A ∈ V
pwslnmlem2.b ⊢ B ∈ V
pwslnmlem2.x ⊢ X = W ↑ 𝑠 A
pwslnmlem2.y ⊢ Y = W ↑ 𝑠 B
pwslnmlem2.z ⊢ Z = W ↑ 𝑠 A ∪ B
pwslnmlem2.w ⊢ φ → W ∈ LMod
pwslnmlem2.dj ⊢ φ → A ∩ B = ∅
pwslnmlem2.xn ⊢ φ → X ∈ LNoeM
pwslnmlem2.yn ⊢ φ → Y ∈ LNoeM
Assertion pwslnmlem2 ⊢ φ → Z ∈ LNoeM

Proof

Step Hyp Ref Expression
1 pwslnmlem2.a ⊢ A ∈ V
2 pwslnmlem2.b ⊢ B ∈ V
3 pwslnmlem2.x ⊢ X = W ↑ 𝑠 A
4 pwslnmlem2.y ⊢ Y = W ↑ 𝑠 B
5 pwslnmlem2.z ⊢ Z = W ↑ 𝑠 A ∪ B
6 pwslnmlem2.w ⊢ φ → W ∈ LMod
7 pwslnmlem2.dj ⊢ φ → A ∩ B = ∅
8 pwslnmlem2.xn ⊢ φ → X ∈ LNoeM
9 pwslnmlem2.yn ⊢ φ → Y ∈ LNoeM
10 1 2 unex ⊢ A ∪ B ∈ V
11 10 a1i ⊢ φ → A ∪ B ∈ V
12 ssun1 ⊢ A ⊆ A ∪ B
13 12 a1i ⊢ φ → A ⊆ A ∪ B
14 eqid ⊢ Base Z = Base Z
15 eqid ⊢ Base X = Base X
16 eqid ⊢ x ∈ Base Z ⟼ x ↾ A = x ∈ Base Z ⟼ x ↾ A
17 5 3 14 15 16 pwssplit3 ⊢ W ∈ LMod ∧ A ∪ B ∈ V ∧ A ⊆ A ∪ B → x ∈ Base Z ⟼ x ↾ A ∈ Z LMHom X
18 6 11 13 17 syl3anc ⊢ φ → x ∈ Base Z ⟼ x ↾ A ∈ Z LMHom X
19 fvex ⊢ 0 X ∈ V
20 16 mptiniseg ⊢ 0 X ∈ V → x ∈ Base Z ⟼ x ↾ A -1 0 X = x ∈ Base Z | x ↾ A = 0 X
21 19 20 ax-mp ⊢ x ∈ Base Z ⟼ x ↾ A -1 0 X = x ∈ Base Z | x ↾ A = 0 X
22 lmodgrp ⊢ W ∈ LMod → W ∈ Grp
23 grpmnd ⊢ W ∈ Grp → W ∈ Mnd
24 6 22 23 3syl ⊢ φ → W ∈ Mnd
25 eqid ⊢ 0 W = 0 W
26 3 25 pws0g ⊢ W ∈ Mnd ∧ A ∈ V → A × 0 W = 0 X
27 24 1 26 sylancl ⊢ φ → A × 0 W = 0 X
28 27 eqcomd ⊢ φ → 0 X = A × 0 W
29 28 eqeq2d ⊢ φ → x ↾ A = 0 X ↔ x ↾ A = A × 0 W
30 29 rabbidv ⊢ φ → x ∈ Base Z | x ↾ A = 0 X = x ∈ Base Z | x ↾ A = A × 0 W
31 21 30 syl5eq ⊢ φ → x ∈ Base Z ⟼ x ↾ A -1 0 X = x ∈ Base Z | x ↾ A = A × 0 W
32 31 oveq2d ⊢ φ → Z ↾ 𝑠 x ∈ Base Z ⟼ x ↾ A -1 0 X = Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W
33 eqid ⊢ x ∈ Base Z | x ↾ A = A × 0 W = x ∈ Base Z | x ↾ A = A × 0 W
34 eqid ⊢ y ∈ x ∈ Base Z | x ↾ A = A × 0 W ⟼ y ↾ B = y ∈ x ∈ Base Z | x ↾ A = A × 0 W ⟼ y ↾ B
35 eqid ⊢ Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W = Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W
36 5 14 25 33 34 3 4 35 pwssplit4 ⊢ W ∈ LMod ∧ A ∪ B ∈ V ∧ A ∩ B = ∅ → y ∈ x ∈ Base Z | x ↾ A = A × 0 W ⟼ y ↾ B ∈ Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W LMIso Y
37 6 11 7 36 syl3anc ⊢ φ → y ∈ x ∈ Base Z | x ↾ A = A × 0 W ⟼ y ↾ B ∈ Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W LMIso Y
38 brlmici ⊢ y ∈ x ∈ Base Z | x ↾ A = A × 0 W ⟼ y ↾ B ∈ Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W LMIso Y → Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W ≃ 𝑚 Y
39 lnmlmic ⊢ Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W ≃ 𝑚 Y → Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W ∈ LNoeM ↔ Y ∈ LNoeM
40 37 38 39 3syl ⊢ φ → Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W ∈ LNoeM ↔ Y ∈ LNoeM
41 9 40 mpbird ⊢ φ → Z ↾ 𝑠 x ∈ Base Z | x ↾ A = A × 0 W ∈ LNoeM
42 32 41 eqeltrd ⊢ φ → Z ↾ 𝑠 x ∈ Base Z ⟼ x ↾ A -1 0 X ∈ LNoeM
43 5 3 14 15 16 pwssplit1 ⊢ W ∈ Mnd ∧ A ∪ B ∈ V ∧ A ⊆ A ∪ B → x ∈ Base Z ⟼ x ↾ A : Base Z ⟶ onto Base X
44 24 11 13 43 syl3anc ⊢ φ → x ∈ Base Z ⟼ x ↾ A : Base Z ⟶ onto Base X
45 forn ⊢ x ∈ Base Z ⟼ x ↾ A : Base Z ⟶ onto Base X → ran ⁡ x ∈ Base Z ⟼ x ↾ A = Base X
46 44 45 syl ⊢ φ → ran ⁡ x ∈ Base Z ⟼ x ↾ A = Base X
47 46 oveq2d ⊢ φ → X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A = X ↾ 𝑠 Base X
48 15 ressid ⊢ X ∈ LNoeM → X ↾ 𝑠 Base X = X
49 8 48 syl ⊢ φ → X ↾ 𝑠 Base X = X
50 47 49 eqtrd ⊢ φ → X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A = X
51 50 8 eqeltrd ⊢ φ → X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A ∈ LNoeM
52 eqid ⊢ 0 X = 0 X
53 eqid ⊢ x ∈ Base Z ⟼ x ↾ A -1 0 X = x ∈ Base Z ⟼ x ↾ A -1 0 X
54 eqid ⊢ Z ↾ 𝑠 x ∈ Base Z ⟼ x ↾ A -1 0 X = Z ↾ 𝑠 x ∈ Base Z ⟼ x ↾ A -1 0 X
55 eqid ⊢ X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A = X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A
56 52 53 54 55 lmhmlnmsplit ⊢ x ∈ Base Z ⟼ x ↾ A ∈ Z LMHom X ∧ Z ↾ 𝑠 x ∈ Base Z ⟼ x ↾ A -1 0 X ∈ LNoeM ∧ X ↾ 𝑠 ran ⁡ x ∈ Base Z ⟼ x ↾ A ∈ LNoeM → Z ∈ LNoeM
57 18 42 51 56 syl3anc ⊢ φ → Z ∈ LNoeM