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 e. LNoeR /\ I e. Fin ) -> Y e. LNoeM )

Proof

Step	Hyp	Ref	Expression
1		lnrfrlm.y	|- Y = ( R freeLMod I )
2	1	frlmpwsfi	|- ( ( R e. LNoeR /\ I e. Fin ) -> Y = ( ( ringLMod ` R ) ^s I ) )
3		lnrlnm	|- ( R e. LNoeR -> ( ringLMod ` R ) e. LNoeM )
4		eqid	|- ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
5	4	pwslnm	|- ( ( ( ringLMod ` R ) e. LNoeM /\ I e. Fin ) -> ( ( ringLMod ` R ) ^s I ) e. LNoeM )
6	3 5	sylan	|- ( ( R e. LNoeR /\ I e. Fin ) -> ( ( ringLMod ` R ) ^s I ) e. LNoeM )
7	2 6	eqeltrd	|- ( ( R e. LNoeR /\ I e. Fin ) -> Y e. LNoeM )