Metamath Proof Explorer

Theorem filnm

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

Ref Expression
Hypothesis filnm.b ⊢ B = Base W
Assertion filnm ⊢ W ∈ LMod ∧ B ∈ Fin → W ∈ LNoeM

Proof

Step Hyp Ref Expression
1 filnm.b ⊢ B = Base W
2 simpl ⊢ W ∈ LMod ∧ B ∈ Fin → W ∈ LMod
3 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
4 1 3 lssss ⊢ a ∈ LSubSp ⁡ W → a ⊆ B
5 4 adantl ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → a ⊆ B
6 velpw ⊢ a ∈ 𝒫 B ↔ a ⊆ B
7 5 6 sylibr ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → a ∈ 𝒫 B
8 simplr ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → B ∈ Fin
9 ssfi ⊢ B ∈ Fin ∧ a ⊆ B → a ∈ Fin
10 8 5 9 syl2anc ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → a ∈ Fin
11 7 10 elind ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → a ∈ 𝒫 B ∩ Fin
12 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
13 3 12 lspid ⊢ W ∈ LMod ∧ a ∈ LSubSp ⁡ W → LSpan ⁡ W ⁡ a = a
14 13 adantlr ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → LSpan ⁡ W ⁡ a = a
15 14 eqcomd ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → a = LSpan ⁡ W ⁡ a
16 fveq2 ⊢ b = a → LSpan ⁡ W ⁡ b = LSpan ⁡ W ⁡ a
17 16 rspceeqv ⊢ a ∈ 𝒫 B ∩ Fin ∧ a = LSpan ⁡ W ⁡ a → ∃ b ∈ 𝒫 B ∩ Fin a = LSpan ⁡ W ⁡ b
18 11 15 17 syl2anc ⊢ W ∈ LMod ∧ B ∈ Fin ∧ a ∈ LSubSp ⁡ W → ∃ b ∈ 𝒫 B ∩ Fin a = LSpan ⁡ W ⁡ b
19 18 ralrimiva ⊢ W ∈ LMod ∧ B ∈ Fin → ∀ a ∈ LSubSp ⁡ W ∃ b ∈ 𝒫 B ∩ Fin a = LSpan ⁡ W ⁡ b
20 1 3 12 islnm2 ⊢ W ∈ LNoeM ↔ W ∈ LMod ∧ ∀ a ∈ LSubSp ⁡ W ∃ b ∈ 𝒫 B ∩ Fin a = LSpan ⁡ W ⁡ b
21 2 19 20 sylanbrc ⊢ W ∈ LMod ∧ B ∈ Fin → W ∈ LNoeM