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	$⊢ U = LIdeal (R)$
	lnr2i.n	$⊢ N = RSpan (R)$
Assertion	lnr2i	$⊢ (R \in LNoeR \land I \in U) \to \exists g \in (𝒫 I \cap Fin) I = N (g)$

Proof

Step	Hyp	Ref	Expression
1		lnr2i.u	$⊢ U = LIdeal (R)$
2		lnr2i.n	$⊢ N = RSpan (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 1 2	islnr2	$⊢ R \in LNoeR \leftrightarrow (R \in Ring \land \forall i \in U \exists g \in (𝒫 {Base}_{R} \cap Fin) i = N (g))$
5	4	simprbi	$⊢ R \in LNoeR \to \forall i \in U \exists g \in (𝒫 {Base}_{R} \cap Fin) i = N (g)$
6		eqeq1	$⊢ i = I \to (i = N (g) \leftrightarrow I = N (g))$
7	6	rexbidv	$⊢ i = I \to (\exists g \in (𝒫 {Base}_{R} \cap Fin) i = N (g) \leftrightarrow \exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g))$
8	7	rspcva	$⊢ (I \in U \land \forall i \in U \exists g \in (𝒫 {Base}_{R} \cap Fin) i = N (g)) \to \exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g)$
9	5 8	sylan2	$⊢ (I \in U \land R \in LNoeR) \to \exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g)$
10	9	ancoms	$⊢ (R \in LNoeR \land I \in U) \to \exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g)$
11		lnrring	$⊢ R \in LNoeR \to R \in Ring$
12	2 3	rspssid	$⊢ (R \in Ring \land g \subseteq {Base}_{R}) \to g \subseteq N (g)$
13	11 12	sylan	$⊢ (R \in LNoeR \land g \subseteq {Base}_{R}) \to g \subseteq N (g)$
14	13	ex	$⊢ R \in LNoeR \to (g \subseteq {Base}_{R} \to g \subseteq N (g))$
15		vex	$⊢ g \in V$
16	15	elpw	$⊢ g \in 𝒫 {Base}_{R} \leftrightarrow g \subseteq {Base}_{R}$
17	15	elpw	$⊢ g \in 𝒫 N (g) \leftrightarrow g \subseteq N (g)$
18	14 16 17	3imtr4g	$⊢ R \in LNoeR \to (g \in 𝒫 {Base}_{R} \to g \in 𝒫 N (g))$
19	18	anim1d	$⊢ R \in LNoeR \to ((g \in 𝒫 {Base}_{R} \land g \in Fin) \to (g \in 𝒫 N (g) \land g \in Fin))$
20		elin	$⊢ g \in (𝒫 {Base}_{R} \cap Fin) \leftrightarrow (g \in 𝒫 {Base}_{R} \land g \in Fin)$
21		elin	$⊢ g \in (𝒫 N (g) \cap Fin) \leftrightarrow (g \in 𝒫 N (g) \land g \in Fin)$
22	19 20 21	3imtr4g	$⊢ R \in LNoeR \to (g \in (𝒫 {Base}_{R} \cap Fin) \to g \in (𝒫 N (g) \cap Fin))$
23		pweq	$⊢ I = N (g) \to 𝒫 I = 𝒫 N (g)$
24	23	ineq1d	$⊢ I = N (g) \to 𝒫 I \cap Fin = 𝒫 N (g) \cap Fin$
25	24	eleq2d	$⊢ I = N (g) \to (g \in (𝒫 I \cap Fin) \leftrightarrow g \in (𝒫 N (g) \cap Fin))$
26	25	imbi2d	$⊢ I = N (g) \to ((g \in (𝒫 {Base}_{R} \cap Fin) \to g \in (𝒫 I \cap Fin)) \leftrightarrow (g \in (𝒫 {Base}_{R} \cap Fin) \to g \in (𝒫 N (g) \cap Fin)))$
27	22 26	syl5ibrcom	$⊢ R \in LNoeR \to (I = N (g) \to (g \in (𝒫 {Base}_{R} \cap Fin) \to g \in (𝒫 I \cap Fin)))$
28	27	imdistand	$⊢ R \in LNoeR \to ((I = N (g) \land g \in (𝒫 {Base}_{R} \cap Fin)) \to (I = N (g) \land g \in (𝒫 I \cap Fin)))$
29		ancom	$⊢ (g \in (𝒫 {Base}_{R} \cap Fin) \land I = N (g)) \leftrightarrow (I = N (g) \land g \in (𝒫 {Base}_{R} \cap Fin))$
30		ancom	$⊢ (g \in (𝒫 I \cap Fin) \land I = N (g)) \leftrightarrow (I = N (g) \land g \in (𝒫 I \cap Fin))$
31	28 29 30	3imtr4g	$⊢ R \in LNoeR \to ((g \in (𝒫 {Base}_{R} \cap Fin) \land I = N (g)) \to (g \in (𝒫 I \cap Fin) \land I = N (g)))$
32	31	reximdv2	$⊢ R \in LNoeR \to (\exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g) \to \exists g \in (𝒫 I \cap Fin) I = N (g))$
33	32	adantr	$⊢ (R \in LNoeR \land I \in U) \to (\exists g \in (𝒫 {Base}_{R} \cap Fin) I = N (g) \to \exists g \in (𝒫 I \cap Fin) I = N (g))$
34	10 33	mpd	$⊢ (R \in LNoeR \land I \in U) \to \exists g \in (𝒫 I \cap Fin) I = N (g)$

Metamath Proof Explorer

Theorem lnr2i

Proof