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 ⊢ B = Base T
Assertion lnmepi ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → T ∈ LNoeM

Proof

Step Hyp Ref Expression
1 lnmepi.b ⊢ B = Base T
2 lmhmlmod2 ⊢ F ∈ S LMHom T → T ∈ LMod
3 2 3ad2ant1 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → T ∈ LMod
4 eqid ⊢ Base S = Base S
5 4 1 lmhmf ⊢ F ∈ S LMHom T → F : Base S ⟶ B
6 5 3ad2ant1 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → F : Base S ⟶ B
7 simp3 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → ran ⁡ F = B
8 dffo2 ⊢ F : Base S ⟶ onto B ↔ F : Base S ⟶ B ∧ ran ⁡ F = B
9 6 7 8 sylanbrc ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → F : Base S ⟶ onto B
10 eqid ⊢ LSubSp ⁡ T = LSubSp ⁡ T
11 1 10 lssss ⊢ a ∈ LSubSp ⁡ T → a ⊆ B
12 foimacnv ⊢ F : Base S ⟶ onto B ∧ a ⊆ B → F F -1 a = a
13 9 11 12 syl2an ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → F F -1 a = a
14 13 oveq2d ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → T ↾ 𝑠 F F -1 a = T ↾ 𝑠 a
15 eqid ⊢ T ↾ 𝑠 F F -1 a = T ↾ 𝑠 F F -1 a
16 eqid ⊢ S ↾ 𝑠 F -1 a = S ↾ 𝑠 F -1 a
17 eqid ⊢ LSubSp ⁡ S = LSubSp ⁡ S
18 simpl2 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → S ∈ LNoeM
19 17 10 lmhmpreima ⊢ F ∈ S LMHom T ∧ a ∈ LSubSp ⁡ T → F -1 a ∈ LSubSp ⁡ S
20 19 3ad2antl1 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → F -1 a ∈ LSubSp ⁡ S
21 17 16 lnmlssfg ⊢ S ∈ LNoeM ∧ F -1 a ∈ LSubSp ⁡ S → S ↾ 𝑠 F -1 a ∈ LFinGen
22 18 20 21 syl2anc ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → S ↾ 𝑠 F -1 a ∈ LFinGen
23 simpl1 ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → F ∈ S LMHom T
24 15 16 17 22 20 23 lmhmfgima ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → T ↾ 𝑠 F F -1 a ∈ LFinGen
25 14 24 eqeltrrd ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B ∧ a ∈ LSubSp ⁡ T → T ↾ 𝑠 a ∈ LFinGen
26 25 ralrimiva ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → ∀ a ∈ LSubSp ⁡ T T ↾ 𝑠 a ∈ LFinGen
27 10 islnm ⊢ T ∈ LNoeM ↔ T ∈ LMod ∧ ∀ a ∈ LSubSp ⁡ T T ↾ 𝑠 a ∈ LFinGen
28 3 26 27 sylanbrc ⊢ F ∈ S LMHom T ∧ S ∈ LNoeM ∧ ran ⁡ F = B → T ∈ LNoeM