Metamath Proof Explorer

Theorem pwslnm

Description: Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis pwslnm.y ⊢ Y = W ↑ 𝑠 I
Assertion pwslnm ⊢ W ∈ LNoeM ∧ I ∈ Fin → Y ∈ LNoeM

Proof

Step Hyp Ref Expression
1 pwslnm.y ⊢ Y = W ↑ 𝑠 I
2 oveq2 ⊢ a = ∅ → W ↑ 𝑠 a = W ↑ 𝑠 ∅
3 2 eleq1d ⊢ a = ∅ → W ↑ 𝑠 a ∈ LNoeM ↔ W ↑ 𝑠 ∅ ∈ LNoeM
4 3 imbi2d ⊢ a = ∅ → W ∈ LNoeM → W ↑ 𝑠 a ∈ LNoeM ↔ W ∈ LNoeM → W ↑ 𝑠 ∅ ∈ LNoeM
5 oveq2 ⊢ a = b → W ↑ 𝑠 a = W ↑ 𝑠 b
6 5 eleq1d ⊢ a = b → W ↑ 𝑠 a ∈ LNoeM ↔ W ↑ 𝑠 b ∈ LNoeM
7 6 imbi2d ⊢ a = b → W ∈ LNoeM → W ↑ 𝑠 a ∈ LNoeM ↔ W ∈ LNoeM → W ↑ 𝑠 b ∈ LNoeM
8 oveq2 ⊢ a = b ∪ c → W ↑ 𝑠 a = W ↑ 𝑠 b ∪ c
9 8 eleq1d ⊢ a = b ∪ c → W ↑ 𝑠 a ∈ LNoeM ↔ W ↑ 𝑠 b ∪ c ∈ LNoeM
10 9 imbi2d ⊢ a = b ∪ c → W ∈ LNoeM → W ↑ 𝑠 a ∈ LNoeM ↔ W ∈ LNoeM → W ↑ 𝑠 b ∪ c ∈ LNoeM
11 oveq2 ⊢ a = I → W ↑ 𝑠 a = W ↑ 𝑠 I
12 11 eleq1d ⊢ a = I → W ↑ 𝑠 a ∈ LNoeM ↔ W ↑ 𝑠 I ∈ LNoeM
13 12 imbi2d ⊢ a = I → W ∈ LNoeM → W ↑ 𝑠 a ∈ LNoeM ↔ W ∈ LNoeM → W ↑ 𝑠 I ∈ LNoeM
14 lnmlmod ⊢ W ∈ LNoeM → W ∈ LMod
15 eqid ⊢ W ↑ 𝑠 ∅ = W ↑ 𝑠 ∅
16 15 pwslnmlem0 ⊢ W ∈ LMod → W ↑ 𝑠 ∅ ∈ LNoeM
17 14 16 syl ⊢ W ∈ LNoeM → W ↑ 𝑠 ∅ ∈ LNoeM
18 vex ⊢ b ∈ V
19 vsnex ⊢ c ∈ V
20 eqid ⊢ W ↑ 𝑠 b = W ↑ 𝑠 b
21 eqid ⊢ W ↑ 𝑠 c = W ↑ 𝑠 c
22 eqid ⊢ W ↑ 𝑠 b ∪ c = W ↑ 𝑠 b ∪ c
23 14 ad2antrl ⊢ b ∈ Fin ∧ ¬ c ∈ b ∧ W ∈ LNoeM ∧ W ↑ 𝑠 b ∈ LNoeM → W ∈ LMod
24 disjsn ⊢ b ∩ c = ∅ ↔ ¬ c ∈ b
25 24 biimpri ⊢ ¬ c ∈ b → b ∩ c = ∅
26 25 ad2antlr ⊢ b ∈ Fin ∧ ¬ c ∈ b ∧ W ∈ LNoeM ∧ W ↑ 𝑠 b ∈ LNoeM → b ∩ c = ∅
27 simprr ⊢ b ∈ Fin ∧ ¬ c ∈ b ∧ W ∈ LNoeM ∧ W ↑ 𝑠 b ∈ LNoeM → W ↑ 𝑠 b ∈ LNoeM
28 21 pwslnmlem1 ⊢ W ∈ LNoeM → W ↑ 𝑠 c ∈ LNoeM
29 28 ad2antrl ⊢ b ∈ Fin ∧ ¬ c ∈ b ∧ W ∈ LNoeM ∧ W ↑ 𝑠 b ∈ LNoeM → W ↑ 𝑠 c ∈ LNoeM
30 18 19 20 21 22 23 26 27 29 pwslnmlem2 ⊢ b ∈ Fin ∧ ¬ c ∈ b ∧ W ∈ LNoeM ∧ W ↑ 𝑠 b ∈ LNoeM → W ↑ 𝑠 b ∪ c ∈ LNoeM
31 30 exp32 ⊢ b ∈ Fin ∧ ¬ c ∈ b → W ∈ LNoeM → W ↑ 𝑠 b ∈ LNoeM → W ↑ 𝑠 b ∪ c ∈ LNoeM
32 31 a2d ⊢ b ∈ Fin ∧ ¬ c ∈ b → W ∈ LNoeM → W ↑ 𝑠 b ∈ LNoeM → W ∈ LNoeM → W ↑ 𝑠 b ∪ c ∈ LNoeM
33 4 7 10 13 17 32 findcard2s ⊢ I ∈ Fin → W ∈ LNoeM → W ↑ 𝑠 I ∈ LNoeM
34 33 impcom ⊢ W ∈ LNoeM ∧ I ∈ Fin → W ↑ 𝑠 I ∈ LNoeM
35 1 34 eqeltrid ⊢ W ∈ LNoeM ∧ I ∈ Fin → Y ∈ LNoeM