Theorem 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	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
Assertion	lnrfg	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM )

Proof

Step	Hyp	Ref	Expression
1		lnrfg.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
2		eqid	⊢ ( 𝑆 freeLMod 𝑎 ) = ( 𝑆 freeLMod 𝑎 )
3		eqid	⊢ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) = ( Base ‘ ( 𝑆 freeLMod 𝑎 ) )
4		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
6		eqid	⊢ ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) )
7		fglmod	⊢ ( 𝑀 ∈ LFinGen → 𝑀 ∈ LMod )
8	7	ad3antrrr	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
9		vex	⊢ 𝑎 ∈ V
10	9	a1i	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ V )
11	1	a1i	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 = ( Scalar ‘ 𝑀 ) )
12		f1oi	⊢ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎
13		f1of	⊢ ( ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 → ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 )
14	12 13	ax-mp	⊢ ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎
15		elpwi	⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → 𝑎 ⊆ ( Base ‘ 𝑀 ) )
16		fss	⊢ ( ( ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 ∧ 𝑎 ⊆ ( Base ‘ 𝑀 ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
17	14 15 16	sylancr	⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
18	17	ad2antlr	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
19	2 3 4 5 6 8 10 11 18	frlmup1	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) )
20		simpllr	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 ∈ LNoeR )
21		simprl	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ Fin )
22	2	lnrfrlm	⊢ ( ( 𝑆 ∈ LNoeR ∧ 𝑎 ∈ Fin ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM )
23	20 21 22	syl2anc	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM )
24		eqid	⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
25	2 3 4 5 6 8 10 11 18 24	frlmup3	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) )
26		rnresi	⊢ ran ( I ↾ 𝑎 ) = 𝑎
27	26	fveq2i	⊢ ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 )
28		simprr	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) )
29	27 28	eqtrid	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( Base ‘ 𝑀 ) )
30	25 29	eqtrd	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) )
31	4	lnmepi	⊢ ( ( ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) ∧ ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM ∧ ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LNoeM )
32	19 23 30 31	syl3anc	⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LNoeM )
33	4 24	islmodfg	⊢ ( 𝑀 ∈ LMod → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) )
34	7 33	syl	⊢ ( 𝑀 ∈ LFinGen → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) )
35	34	ibi	⊢ ( 𝑀 ∈ LFinGen → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) )
36	35	adantr	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) )
37	32 36	r19.29a	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM )