Metamath Proof Explorer

Theorem lnrfrlm

Description: Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypothesis lnrfrlm.y ⊢ Y = R freeLMod I
Assertion lnrfrlm ⊢ R ∈ LNoeR ∧ I ∈ Fin → Y ∈ LNoeM

Proof

Step Hyp Ref Expression
1 lnrfrlm.y ⊢ Y = R freeLMod I
2 1 frlmpwsfi ⊢ R ∈ LNoeR ∧ I ∈ Fin → Y = ringLMod ⁡ R ↑ 𝑠 I
3 lnrlnm ⊢ R ∈ LNoeR → ringLMod ⁡ R ∈ LNoeM
4 eqid ⊢ ringLMod ⁡ R ↑ 𝑠 I = ringLMod ⁡ R ↑ 𝑠 I
5 4 pwslnm ⊢ ringLMod ⁡ R ∈ LNoeM ∧ I ∈ Fin → ringLMod ⁡ R ↑ 𝑠 I ∈ LNoeM
6 3 5 sylan ⊢ R ∈ LNoeR ∧ I ∈ Fin → ringLMod ⁡ R ↑ 𝑠 I ∈ LNoeM
7 2 6 eqeltrd ⊢ R ∈ LNoeR ∧ I ∈ Fin → Y ∈ LNoeM