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 )