Theorem lnr2i

Description: Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Hypotheses	lnr2i.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lnr2i.n	⊢ 𝑁 = ( RSpan ‘ 𝑅 )
Assertion	lnr2i	⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ) → ∃ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		lnr2i.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lnr2i.n	⊢ 𝑁 = ( RSpan ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 1 2	islnr2	⊢ ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
5	4	simprbi	⊢ ( 𝑅 ∈ LNoeR → ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) )
6		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = ( 𝑁 ‘ 𝑔 ) ↔ 𝐼 = ( 𝑁 ‘ 𝑔 ) ) )
7	6	rexbidv	⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) ) )
8	7	rspcva	⊢ ( ( 𝐼 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) → ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) )
9	5 8	sylan2	⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝑅 ∈ LNoeR ) → ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) )
10	9	ancoms	⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ) → ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) )
11		lnrring	⊢ ( 𝑅 ∈ LNoeR → 𝑅 ∈ Ring )
12	2 3	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑔 ⊆ ( Base ‘ 𝑅 ) ) → 𝑔 ⊆ ( 𝑁 ‘ 𝑔 ) )
13	11 12	sylan	⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝑔 ⊆ ( Base ‘ 𝑅 ) ) → 𝑔 ⊆ ( 𝑁 ‘ 𝑔 ) )
14	13	ex	⊢ ( 𝑅 ∈ LNoeR → ( 𝑔 ⊆ ( Base ‘ 𝑅 ) → 𝑔 ⊆ ( 𝑁 ‘ 𝑔 ) ) )
15		vex	⊢ 𝑔 ∈ V
16	15	elpw	⊢ ( 𝑔 ∈ 𝒫 ( Base ‘ 𝑅 ) ↔ 𝑔 ⊆ ( Base ‘ 𝑅 ) )
17	15	elpw	⊢ ( 𝑔 ∈ 𝒫 ( 𝑁 ‘ 𝑔 ) ↔ 𝑔 ⊆ ( 𝑁 ‘ 𝑔 ) )
18	14 16 17	3imtr4g	⊢ ( 𝑅 ∈ LNoeR → ( 𝑔 ∈ 𝒫 ( Base ‘ 𝑅 ) → 𝑔 ∈ 𝒫 ( 𝑁 ‘ 𝑔 ) ) )
19	18	anim1d	⊢ ( 𝑅 ∈ LNoeR → ( ( 𝑔 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ 𝑔 ∈ Fin ) → ( 𝑔 ∈ 𝒫 ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ Fin ) ) )
20		elin	⊢ ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ↔ ( 𝑔 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ 𝑔 ∈ Fin ) )
21		elin	⊢ ( 𝑔 ∈ ( 𝒫 ( 𝑁 ‘ 𝑔 ) ∩ Fin ) ↔ ( 𝑔 ∈ 𝒫 ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ Fin ) )
22	19 20 21	3imtr4g	⊢ ( 𝑅 ∈ LNoeR → ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) → 𝑔 ∈ ( 𝒫 ( 𝑁 ‘ 𝑔 ) ∩ Fin ) ) )
23		pweq	⊢ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) → 𝒫 𝐼 = 𝒫 ( 𝑁 ‘ 𝑔 ) )
24	23	ineq1d	⊢ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) → ( 𝒫 𝐼 ∩ Fin ) = ( 𝒫 ( 𝑁 ‘ 𝑔 ) ∩ Fin ) )
25	24	eleq2d	⊢ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) → ( 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ↔ 𝑔 ∈ ( 𝒫 ( 𝑁 ‘ 𝑔 ) ∩ Fin ) ) )
26	25	imbi2d	⊢ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) → ( ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) → 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ) ↔ ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) → 𝑔 ∈ ( 𝒫 ( 𝑁 ‘ 𝑔 ) ∩ Fin ) ) ) )
27	22 26	syl5ibrcom	⊢ ( 𝑅 ∈ LNoeR → ( 𝐼 = ( 𝑁 ‘ 𝑔 ) → ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) → 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ) ) )
28	27	imdistand	⊢ ( 𝑅 ∈ LNoeR → ( ( 𝐼 = ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ) → ( 𝐼 = ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ) ) )
29		ancom	⊢ ( ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ∧ 𝐼 = ( 𝑁 ‘ 𝑔 ) ) ↔ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ) )
30		ancom	⊢ ( ( 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ 𝐼 = ( 𝑁 ‘ 𝑔 ) ) ↔ ( 𝐼 = ( 𝑁 ‘ 𝑔 ) ∧ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ) )
31	28 29 30	3imtr4g	⊢ ( 𝑅 ∈ LNoeR → ( ( 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ∧ 𝐼 = ( 𝑁 ‘ 𝑔 ) ) → ( 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ 𝐼 = ( 𝑁 ‘ 𝑔 ) ) ) )
32	31	reximdv2	⊢ ( 𝑅 ∈ LNoeR → ( ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) → ∃ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) ) )
33	32	adantr	⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ) → ( ∃ 𝑔 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) → ∃ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) ) )
34	10 33	mpd	⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ) → ∃ 𝑔 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐼 = ( 𝑁 ‘ 𝑔 ) )