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 \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to T \in LNoeM$

Proof

Step	Hyp	Ref	Expression
1		lnmepi.b	$⊢ B = {Base}_{T}$
2		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
3	2	3ad2ant1	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to T \in LMod$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5	4 1	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ B$
6	5	3ad2ant1	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to F : {Base}_{S} ⟶ B$
7		simp3	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to ran F = B$
8		dffo2	$⊢ F : {Base}_{S} \underset{onto}{⟶} B \leftrightarrow (F : {Base}_{S} ⟶ B \land ran F = B)$
9	6 7 8	sylanbrc	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to F : {Base}_{S} \underset{onto}{⟶} B$
10		eqid	$⊢ LSubSp (T) = LSubSp (T)$
11	1 10	lssss	$⊢ a \in LSubSp (T) \to a \subseteq B$
12		foimacnv	$⊢ (F : {Base}_{S} \underset{onto}{⟶} B \land a \subseteq B) \to F [F^{-1} [a]] = a$
13	9 11 12	syl2an	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to F [F^{-1} [a]] = a$
14	13	oveq2d	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to 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 \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to S \in LNoeM$
19	17 10	lmhmpreima	$⊢ (F \in (S LMHom T) \land a \in LSubSp (T)) \to F^{-1} [a] \in LSubSp (S)$
20	19	3ad2antl1	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to F^{-1} [a] \in LSubSp (S)$
21	17 16	lnmlssfg	$⊢ (S \in LNoeM \land F^{-1} [a] \in LSubSp (S)) \to S ↾_{𝑠} F^{-1} [a] \in LFinGen$
22	18 20 21	syl2anc	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to S ↾_{𝑠} F^{-1} [a] \in LFinGen$
23		simpl1	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to F \in (S LMHom T)$
24	15 16 17 22 20 23	lmhmfgima	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to T ↾_{𝑠} F [F^{-1} [a]] \in LFinGen$
25	14 24	eqeltrrd	$⊢ ((F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \land a \in LSubSp (T)) \to T ↾_{𝑠} a \in LFinGen$
26	25	ralrimiva	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to \forall a \in LSubSp (T) T ↾_{𝑠} a \in LFinGen$
27	10	islnm	$⊢ T \in LNoeM \leftrightarrow (T \in LMod \land \forall a \in LSubSp (T) T ↾_{𝑠} a \in LFinGen)$
28	3 26 27	sylanbrc	$⊢ (F \in (S LMHom T) \land S \in LNoeM \land ran F = B) \to T \in LNoeM$

Metamath Proof Explorer

Theorem lnmepi

Proof