Metamath Proof Explorer

Theorem lnmepi

Description: Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis lnmepi.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
Assertion lnmepi ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → 𝑇 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 lnmepi.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
2 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
3 2 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → 𝑇 ∈ LMod )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 4 1 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝐵 )
6 5 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝐵 )
7 simp3 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → ran 𝐹 = 𝐵 )
8 dffo2 ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) –onto→ 𝐵 ↔ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
9 6 7 8 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → 𝐹 : ( Base ‘ 𝑆 ) –onto→ 𝐵 )
10 eqid ⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
11 1 10 lssss ⊢ ( 𝑎 ∈ ( LSubSp ‘ 𝑇 ) → 𝑎 ⊆ 𝐵 )
12 foimacnv ⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) –onto→ 𝐵 ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) = 𝑎 )
13 9 11 12 syl2an ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) = 𝑎 )
14 13 oveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝑇 ↾s ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) ) = ( 𝑇 ↾s 𝑎 ) )
15 eqid ⊢ ( 𝑇 ↾s ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) ) = ( 𝑇 ↾s ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) )
16 eqid ⊢ ( 𝑆 ↾s ( ◡ 𝐹 “ 𝑎 ) ) = ( 𝑆 ↾s ( ◡ 𝐹 “ 𝑎 ) )
17 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
18 simpl2 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → 𝑆 ∈ LNoeM )
19 17 10 lmhmpreima ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( ◡ 𝐹 “ 𝑎 ) ∈ ( LSubSp ‘ 𝑆 ) )
20 19 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( ◡ 𝐹 “ 𝑎 ) ∈ ( LSubSp ‘ 𝑆 ) )
21 17 16 lnmlssfg ⊢ ( ( 𝑆 ∈ LNoeM ∧ ( ◡ 𝐹 “ 𝑎 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑆 ↾s ( ◡ 𝐹 “ 𝑎 ) ) ∈ LFinGen )
22 18 20 21 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝑆 ↾s ( ◡ 𝐹 “ 𝑎 ) ) ∈ LFinGen )
23 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
24 15 16 17 22 20 23 lmhmfgima ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝑇 ↾s ( 𝐹 “ ( ◡ 𝐹 “ 𝑎 ) ) ) ∈ LFinGen )
25 14 24 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝑇 ↾s 𝑎 ) ∈ LFinGen )
26 25 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → ∀ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ( 𝑇 ↾s 𝑎 ) ∈ LFinGen )
27 10 islnm ⊢ ( 𝑇 ∈ LNoeM ↔ ( 𝑇 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑇 ) ( 𝑇 ↾s 𝑎 ) ∈ LFinGen ) )
28 3 26 27 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵 ) → 𝑇 ∈ LNoeM )