lnmlsslnm

Description: All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lnmlssfg.s	$⊢ S = LSubSp (M)$
	lnmlssfg.r	$⊢ R = M ↾_{𝑠} U$
Assertion	lnmlsslnm	$⊢ (M \in LNoeM \land U \in S) \to R \in LNoeM$

Proof

Step	Hyp	Ref	Expression
1		lnmlssfg.s	$⊢ S = LSubSp (M)$
2		lnmlssfg.r	$⊢ R = M ↾_{𝑠} U$
3		lnmlmod	$⊢ M \in LNoeM \to M \in LMod$
4	2 1	lsslmod	$⊢ (M \in LMod \land U \in S) \to R \in LMod$
5	3 4	sylan	$⊢ (M \in LNoeM \land U \in S) \to R \in LMod$
6	2	oveq1i	$⊢ R ↾_{𝑠} a = (M ↾_{𝑠} U) ↾_{𝑠} a$
7		simplr	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to U \in S$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ LSubSp (R) = LSubSp (R)$
10	8 9	lssss	$⊢ a \in LSubSp (R) \to a \subseteq {Base}_{R}$
11	10	adantl	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to a \subseteq {Base}_{R}$
12		eqid	$⊢ {Base}_{M} = {Base}_{M}$
13	12 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{M}$
14	2 12	ressbas2	$⊢ U \subseteq {Base}_{M} \to U = {Base}_{R}$
15	13 14	syl	$⊢ U \in S \to U = {Base}_{R}$
16	15	ad2antlr	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to U = {Base}_{R}$
17	11 16	sseqtrrd	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to a \subseteq U$
18		ressabs	$⊢ (U \in S \land a \subseteq U) \to (M ↾_{𝑠} U) ↾_{𝑠} a = M ↾_{𝑠} a$
19	7 17 18	syl2anc	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to (M ↾_{𝑠} U) ↾_{𝑠} a = M ↾_{𝑠} a$
20	6 19	syl5eq	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to R ↾_{𝑠} a = M ↾_{𝑠} a$
21		simpll	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to M \in LNoeM$
22	2 1 9	lsslss	$⊢ (M \in LMod \land U \in S) \to (a \in LSubSp (R) \leftrightarrow (a \in S \land a \subseteq U))$
23	3 22	sylan	$⊢ (M \in LNoeM \land U \in S) \to (a \in LSubSp (R) \leftrightarrow (a \in S \land a \subseteq U))$
24	23	simprbda	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to a \in S$
25		eqid	$⊢ M ↾_{𝑠} a = M ↾_{𝑠} a$
26	1 25	lnmlssfg	$⊢ (M \in LNoeM \land a \in S) \to M ↾_{𝑠} a \in LFinGen$
27	21 24 26	syl2anc	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to M ↾_{𝑠} a \in LFinGen$
28	20 27	eqeltrd	$⊢ ((M \in LNoeM \land U \in S) \land a \in LSubSp (R)) \to R ↾_{𝑠} a \in LFinGen$
29	28	ralrimiva	$⊢ (M \in LNoeM \land U \in S) \to \forall a \in LSubSp (R) R ↾_{𝑠} a \in LFinGen$
30	9	islnm	$⊢ R \in LNoeM \leftrightarrow (R \in LMod \land \forall a \in LSubSp (R) R ↾_{𝑠} a \in LFinGen)$
31	5 29 30	sylanbrc	$⊢ (M \in LNoeM \land U \in S) \to R \in LNoeM$

Metamath Proof Explorer

Theorem lnmlsslnm

Proof