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 ) |
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 ) |