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 )