Metamath Proof Explorer


Theorem filnm

Description: Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis filnm.b 𝐵 = ( Base ‘ 𝑊 )
Assertion filnm ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 filnm.b 𝐵 = ( Base ‘ 𝑊 )
2 simpl ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LMod )
3 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
4 1 3 lssss ( 𝑎 ∈ ( LSubSp ‘ 𝑊 ) → 𝑎𝐵 )
5 4 adantl ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎𝐵 )
6 velpw ( 𝑎 ∈ 𝒫 𝐵𝑎𝐵 )
7 5 6 sylibr ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ 𝒫 𝐵 )
8 simplr ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝐵 ∈ Fin )
9 ssfi ( ( 𝐵 ∈ Fin ∧ 𝑎𝐵 ) → 𝑎 ∈ Fin )
10 8 5 9 syl2anc ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ Fin )
11 7 10 elind ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) )
12 eqid ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
13 3 12 lspid ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) = 𝑎 )
14 13 adantlr ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) = 𝑎 )
15 14 eqcomd ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) )
16 fveq2 ( 𝑏 = 𝑎 → ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) )
17 16 rspceeqv ( ( 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) )
18 11 15 17 syl2anc ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) )
19 18 ralrimiva ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → ∀ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) )
20 1 3 12 islnm2 ( 𝑊 ∈ LNoeM ↔ ( 𝑊 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) ) )
21 2 19 20 sylanbrc ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LNoeM )