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 )