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=BaseW
Assertion filnm ⊢W∈LMod∧B∈Fin→W∈LNoeM

Proof

Step Hyp Ref Expression
1 filnm.b ⊢B=BaseW
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∩Fina=LSpan⁡W⁡b
18 11 15 17 syl2anc ⊢W∈LMod∧B∈Fin∧a∈LSubSp⁡W→∃b∈𝒫B∩Fina=LSpan⁡W⁡b
19 18 ralrimiva ⊢W∈LMod∧B∈Fin→∀a∈LSubSp⁡W∃b∈𝒫B∩Fina=LSpan⁡W⁡b
20 1 3 12 islnm2 ⊢W∈LNoeM↔W∈LMod∧∀a∈LSubSp⁡W∃b∈𝒫B∩Fina=LSpan⁡W⁡b
21 2 19 20 sylanbrc ⊢W∈LMod∧B∈Fin→W∈LNoeM