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 𝑌 = ( 𝑅 freeLMod 𝐼 )
Assertion lnrfrlm ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin ) → 𝑌 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 lnrfrlm.y 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 1 frlmpwsfi ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin ) → 𝑌 = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
3 lnrlnm ( 𝑅 ∈ LNoeR → ( ringLMod ‘ 𝑅 ) ∈ LNoeM )
4 eqid ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
5 4 pwslnm ( ( ( ringLMod ‘ 𝑅 ) ∈ LNoeM ∧ 𝐼 ∈ Fin ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LNoeM )
6 3 5 sylan ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LNoeM )
7 2 6 eqeltrd ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin ) → 𝑌 ∈ LNoeM )