lnrfg

Description: Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015)

		Ref	Expression
	Hypothesis	lnrfg.s	$⊢ S = Scalar (M)$
	Assertion	lnrfg	$⊢ (M \in LFinGen \land S \in LNoeR) \to M \in LNoeM$

Proof

Step	Hyp	Ref	Expression
1		lnrfg.s	$⊢ S = Scalar (M)$
2		eqid	$⊢ S freeLMod a = S freeLMod a$
3		eqid	$⊢ {Base}_{(S freeLMod a)} = {Base}_{(S freeLMod a)}$
4		eqid	$⊢ {Base}_{M} = {Base}_{M}$
5		eqid	$⊢ \cdot_{M} = \cdot_{M}$
6		eqid	$⊢ (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) = (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a})))$
7		fglmod	$⊢ M \in LFinGen \to M \in LMod$
8	7	ad3antrrr	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to M \in LMod$
9		vex	$⊢ a \in V$
10	9	a1i	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to a \in V$
11	1	a1i	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to S = Scalar (M)$
12		f1oi	$⊢ ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a$
13		f1of	$⊢ ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a \to ({I ↾}_{a}) : a ⟶ a$
14	12 13	ax-mp	$⊢ ({I ↾}_{a}) : a ⟶ a$
15		elpwi	$⊢ a \in 𝒫 {Base}_{M} \to a \subseteq {Base}_{M}$
16		fss	$⊢ (({I ↾}_{a}) : a ⟶ a \land a \subseteq {Base}_{M}) \to ({I ↾}_{a}) : a ⟶ {Base}_{M}$
17	14 15 16	sylancr	$⊢ a \in 𝒫 {Base}_{M} \to ({I ↾}_{a}) : a ⟶ {Base}_{M}$
18	17	ad2antlr	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to ({I ↾}_{a}) : a ⟶ {Base}_{M}$
19	2 3 4 5 6 8 10 11 18	frlmup1	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) \in ((S freeLMod a) LMHom M)$
20		simpllr	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to S \in LNoeR$
21		simprl	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to a \in Fin$
22	2	lnrfrlm	$⊢ (S \in LNoeR \land a \in Fin) \to S freeLMod a \in LNoeM$
23	20 21 22	syl2anc	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to S freeLMod a \in LNoeM$
24		eqid	$⊢ LSpan (M) = LSpan (M)$
25	2 3 4 5 6 8 10 11 18 24	frlmup3	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to ran (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) = LSpan (M) (ran ({I ↾}_{a}))$
26		rnresi	$⊢ ran ({I ↾}_{a}) = a$
27	26	fveq2i	$⊢ LSpan (M) (ran ({I ↾}_{a})) = LSpan (M) (a)$
28		simprr	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to LSpan (M) (a) = {Base}_{M}$
29	27 28	eqtrid	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to LSpan (M) (ran ({I ↾}_{a})) = {Base}_{M}$
30	25 29	eqtrd	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to ran (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) = {Base}_{M}$
31	4	lnmepi	$⊢ ((b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) \in ((S freeLMod a) LMHom M) \land S freeLMod a \in LNoeM \land ran (b \in {Base}_{(S freeLMod a)} ⟼ \sum_{M} (b {\cdot_{M}}_{f} ({I ↾}_{a}))) = {Base}_{M}) \to M \in LNoeM$
32	19 23 30 31	syl3anc	$⊢ (((M \in LFinGen \land S \in LNoeR) \land a \in 𝒫 {Base}_{M}) \land (a \in Fin \land LSpan (M) (a) = {Base}_{M})) \to M \in LNoeM$
33	4 24	islmodfg	$⊢ M \in LMod \to (M \in LFinGen \leftrightarrow \exists a \in 𝒫 {Base}_{M} (a \in Fin \land LSpan (M) (a) = {Base}_{M}))$
34	7 33	syl	$⊢ M \in LFinGen \to (M \in LFinGen \leftrightarrow \exists a \in 𝒫 {Base}_{M} (a \in Fin \land LSpan (M) (a) = {Base}_{M}))$
35	34	ibi	$⊢ M \in LFinGen \to \exists a \in 𝒫 {Base}_{M} (a \in Fin \land LSpan (M) (a) = {Base}_{M})$
36	35	adantr	$⊢ (M \in LFinGen \land S \in LNoeR) \to \exists a \in 𝒫 {Base}_{M} (a \in Fin \land LSpan (M) (a) = {Base}_{M})$
37	32 36	r19.29a	$⊢ (M \in LFinGen \land S \in LNoeR) \to M \in LNoeM$

Metamath Proof Explorer

Theorem lnrfg

Proof