hbt

Description: The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015)

		Ref	Expression
	Hypothesis	hbt.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	hbt	$⊢ R \in LNoeR \to P \in LNoeR$

Proof

Step	Hyp	Ref	Expression
1		hbt.p	$⊢ P = {Poly}_{1} (R)$
2		lnrring	$⊢ R \in LNoeR \to R \in Ring$
3	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
4	2 3	syl	$⊢ R \in LNoeR \to P \in Ring$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ LIdeal (R) = LIdeal (R)$
7	5 6	islnr3	$⊢ R \in LNoeR \leftrightarrow (R \in Ring \land LIdeal (R) \in NoeACS ({Base}_{R}))$
8	7	simprbi	$⊢ R \in LNoeR \to LIdeal (R) \in NoeACS ({Base}_{R})$
9	8	adantr	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to LIdeal (R) \in NoeACS ({Base}_{R})$
10		eqid	$⊢ LIdeal (P) = LIdeal (P)$
11		eqid	$⊢ ldgIdlSeq (R) = ldgIdlSeq (R)$
12	1 10 11 6	hbtlem7	$⊢ (R \in Ring \land a \in LIdeal (P)) \to ldgIdlSeq (R) (a) : ℕ_{0} ⟶ LIdeal (R)$
13	2 12	sylan	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to ldgIdlSeq (R) (a) : ℕ_{0} ⟶ LIdeal (R)$
14	2	ad2antrr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to R \in Ring$
15		simplr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to a \in LIdeal (P)$
16		simpr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to b \in ℕ_{0}$
17		peano2nn0	$⊢ b \in ℕ_{0} \to b + 1 \in ℕ_{0}$
18	17	adantl	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to b + 1 \in ℕ_{0}$
19		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
20	19	lep1d	$⊢ b \in ℕ_{0} \to b \leq b + 1$
21	20	adantl	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to b \leq b + 1$
22	1 10 11 14 15 16 18 21	hbtlem4	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land b \in ℕ_{0}) \to ldgIdlSeq (R) (a) (b) \subseteq ldgIdlSeq (R) (a) (b + 1)$
23	22	ralrimiva	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to \forall b \in ℕ_{0} ldgIdlSeq (R) (a) (b) \subseteq ldgIdlSeq (R) (a) (b + 1)$
24		nacsfix	$⊢ (LIdeal (R) \in NoeACS ({Base}_{R}) \land ldgIdlSeq (R) (a) : ℕ_{0} ⟶ LIdeal (R) \land \forall b \in ℕ_{0} ldgIdlSeq (R) (a) (b) \subseteq ldgIdlSeq (R) (a) (b + 1)) \to \exists c \in ℕ_{0} \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c)$
25	9 13 23 24	syl3anc	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to \exists c \in ℕ_{0} \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c)$
26		fzfi	$⊢ (0 \dots c) \in Fin$
27		eqid	$⊢ RSpan (P) = RSpan (P)$
28		simpll	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land e \in (0 \dots c)) \to R \in LNoeR$
29		simplr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land e \in (0 \dots c)) \to a \in LIdeal (P)$
30		elfznn0	$⊢ e \in (0 \dots c) \to e \in ℕ_{0}$
31	30	adantl	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land e \in (0 \dots c)) \to e \in ℕ_{0}$
32	1 10 11 27 28 29 31	hbtlem6	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land e \in (0 \dots c)) \to \exists b \in (𝒫 a \cap Fin) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (b)) (e)$
33	32	ralrimiva	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to \forall e \in (0 \dots c) \exists b \in (𝒫 a \cap Fin) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (b)) (e)$
34		2fveq3	$⊢ b = f (e) \to ldgIdlSeq (R) (RSpan (P) (b)) = ldgIdlSeq (R) (RSpan (P) (f (e)))$
35	34	fveq1d	$⊢ b = f (e) \to ldgIdlSeq (R) (RSpan (P) (b)) (e) = ldgIdlSeq (R) (RSpan (P) (f (e))) (e)$
36	35	sseq2d	$⊢ b = f (e) \to (ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (b)) (e) \leftrightarrow ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))$
37	36	ac6sfi	$⊢ ((0 \dots c) \in Fin \land \forall e \in (0 \dots c) \exists b \in (𝒫 a \cap Fin) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (b)) (e)) \to \exists f (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))$
38	26 33 37	sylancr	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to \exists f (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))$
39	38	adantr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \to \exists f (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))$
40		frn	$⊢ f : (0 \dots c) ⟶ 𝒫 a \cap Fin \to ran f \subseteq 𝒫 a \cap Fin$
41	40	ad2antrl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ran f \subseteq 𝒫 a \cap Fin$
42		inss1	$⊢ 𝒫 a \cap Fin \subseteq 𝒫 a$
43	41 42	sstrdi	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ran f \subseteq 𝒫 a$
44	43	unissd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \subseteq ⋃ 𝒫 a$
45		unipw	$⊢ ⋃ 𝒫 a = a$
46	44 45	sseqtrdi	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \subseteq a$
47		simpllr	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to a \in LIdeal (P)$
48		eqid	$⊢ {Base}_{P} = {Base}_{P}$
49	48 10	lidlss	$⊢ a \in LIdeal (P) \to a \subseteq {Base}_{P}$
50	47 49	syl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to a \subseteq {Base}_{P}$
51	46 50	sstrd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \subseteq {Base}_{P}$
52		fvex	$⊢ {Base}_{P} \in V$
53	52	elpw2	$⊢ ⋃ ran f \in 𝒫 {Base}_{P} \leftrightarrow ⋃ ran f \subseteq {Base}_{P}$
54	51 53	sylibr	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \in 𝒫 {Base}_{P}$
55		simprl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to f : (0 \dots c) ⟶ 𝒫 a \cap Fin$
56		ffn	$⊢ f : (0 \dots c) ⟶ 𝒫 a \cap Fin \to f Fn (0 \dots c)$
57		fniunfv	$⊢ f Fn (0 \dots c) \to ⋃_{g = 0}^{c} f (g) = ⋃ ran f$
58	55 56 57	3syl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃_{g = 0}^{c} f (g) = ⋃ ran f$
59		inss2	$⊢ 𝒫 a \cap Fin \subseteq Fin$
60	55	ffvelrnda	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in (0 \dots c)) \to f (g) \in (𝒫 a \cap Fin)$
61	59 60	sselid	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in (0 \dots c)) \to f (g) \in Fin$
62	61	ralrimiva	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to \forall g \in (0 \dots c) f (g) \in Fin$
63		iunfi	$⊢ ((0 \dots c) \in Fin \land \forall g \in (0 \dots c) f (g) \in Fin) \to ⋃_{g = 0}^{c} f (g) \in Fin$
64	26 62 63	sylancr	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃_{g = 0}^{c} f (g) \in Fin$
65	58 64	eqeltrrd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \in Fin$
66	54 65	elind	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \in (𝒫 {Base}_{P} \cap Fin)$
67	2	ad3antrrr	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to R \in Ring$
68	4	ad3antrrr	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to P \in Ring$
69	27 48 10	rspcl	$⊢ (P \in Ring \land ⋃ ran f \subseteq {Base}_{P}) \to RSpan (P) (⋃ ran f) \in LIdeal (P)$
70	68 51 69	syl2anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to RSpan (P) (⋃ ran f) \in LIdeal (P)$
71	27 10	rspssp	$⊢ (P \in Ring \land a \in LIdeal (P) \land ⋃ ran f \subseteq a) \to RSpan (P) (⋃ ran f) \subseteq a$
72	68 47 46 71	syl3anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to RSpan (P) (⋃ ran f) \subseteq a$
73		nn0re	$⊢ g \in ℕ_{0} \to g \in ℝ$
74	73	adantl	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \to g \in ℝ$
75		simplrl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to c \in ℕ_{0}$
76	75	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \to c \in ℕ_{0}$
77	76	nn0red	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \to c \in ℝ$
78		simprl	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to g \in ℕ_{0}$
79		simprr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to g \leq c$
80	75	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to c \in ℕ_{0}$
81		fznn0	$⊢ c \in ℕ_{0} \to (g \in (0 \dots c) \leftrightarrow (g \in ℕ_{0} \land g \leq c))$
82	80 81	syl	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to (g \in (0 \dots c) \leftrightarrow (g \in ℕ_{0} \land g \leq c))$
83	78 79 82	mpbir2and	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to g \in (0 \dots c)$
84		simplrr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e)$
85		fveq2	$⊢ e = g \to ldgIdlSeq (R) (a) (e) = ldgIdlSeq (R) (a) (g)$
86		2fveq3	$⊢ e = g \to RSpan (P) (f (e)) = RSpan (P) (f (g))$
87	86	fveq2d	$⊢ e = g \to ldgIdlSeq (R) (RSpan (P) (f (e))) = ldgIdlSeq (R) (RSpan (P) (f (g)))$
88		id	$⊢ e = g \to e = g$
89	87 88	fveq12d	$⊢ e = g \to ldgIdlSeq (R) (RSpan (P) (f (e))) (e) = ldgIdlSeq (R) (RSpan (P) (f (g))) (g)$
90	85 89	sseq12d	$⊢ e = g \to (ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e) \leftrightarrow ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (f (g))) (g))$
91	90	rspcva	$⊢ (g \in (0 \dots c) \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e)) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (f (g))) (g)$
92	83 84 91	syl2anc	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (f (g))) (g)$
93	67	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to R \in Ring$
94		fvssunirn	$⊢ f (g) \subseteq ⋃ ran f$
95	94 51	sstrid	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to f (g) \subseteq {Base}_{P}$
96	27 48 10	rspcl	$⊢ (P \in Ring \land f (g) \subseteq {Base}_{P}) \to RSpan (P) (f (g)) \in LIdeal (P)$
97	68 95 96	syl2anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to RSpan (P) (f (g)) \in LIdeal (P)$
98	97	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to RSpan (P) (f (g)) \in LIdeal (P)$
99	70	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to RSpan (P) (⋃ ran f) \in LIdeal (P)$
100	67 3	syl	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to P \in Ring$
101	100	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to P \in Ring$
102	27 48	rspssid	$⊢ (P \in Ring \land ⋃ ran f \subseteq {Base}_{P}) \to ⋃ ran f \subseteq RSpan (P) (⋃ ran f)$
103	68 51 102	syl2anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ⋃ ran f \subseteq RSpan (P) (⋃ ran f)$
104	103	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to ⋃ ran f \subseteq RSpan (P) (⋃ ran f)$
105	94 104	sstrid	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to f (g) \subseteq RSpan (P) (⋃ ran f)$
106	27 10	rspssp	$⊢ (P \in Ring \land RSpan (P) (⋃ ran f) \in LIdeal (P) \land f (g) \subseteq RSpan (P) (⋃ ran f)) \to RSpan (P) (f (g)) \subseteq RSpan (P) (⋃ ran f)$
107	101 99 105 106	syl3anc	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to RSpan (P) (f (g)) \subseteq RSpan (P) (⋃ ran f)$
108	1 10 11 93 98 99 107 78	hbtlem3	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to ldgIdlSeq (R) (RSpan (P) (f (g))) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
109	92 108	sstrd	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land g \leq c)) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
110	109	anassrs	$⊢ (((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \land g \leq c) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
111		nn0z	$⊢ c \in ℕ_{0} \to c \in ℤ$
112	111	adantr	$⊢ (c \in ℕ_{0} \land (g \in ℕ_{0} \land c \leq g)) \to c \in ℤ$
113		nn0z	$⊢ g \in ℕ_{0} \to g \in ℤ$
114	113	ad2antrl	$⊢ (c \in ℕ_{0} \land (g \in ℕ_{0} \land c \leq g)) \to g \in ℤ$
115		simprr	$⊢ (c \in ℕ_{0} \land (g \in ℕ_{0} \land c \leq g)) \to c \leq g$
116		eluz2	$⊢ g \in ℤ_{\geq c} \leftrightarrow (c \in ℤ \land g \in ℤ \land c \leq g)$
117	112 114 115 116	syl3anbrc	$⊢ (c \in ℕ_{0} \land (g \in ℕ_{0} \land c \leq g)) \to g \in ℤ_{\geq c}$
118	75 117	sylan	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to g \in ℤ_{\geq c}$
119		simprr	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \to \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c)$
120	119	ad2antrr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c)$
121		fveqeq2	$⊢ d = g \to (ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c) \leftrightarrow ldgIdlSeq (R) (a) (g) = ldgIdlSeq (R) (a) (c))$
122	121	rspcva	$⊢ (g \in ℤ_{\geq c} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c)) \to ldgIdlSeq (R) (a) (g) = ldgIdlSeq (R) (a) (c)$
123	118 120 122	syl2anc	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to ldgIdlSeq (R) (a) (g) = ldgIdlSeq (R) (a) (c)$
124	75	nn0red	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to c \in ℝ$
125	124	leidd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to c \leq c$
126	109	expr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \to (g \leq c \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g))$
127	126	ralrimiva	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to \forall g \in ℕ_{0} (g \leq c \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g))$
128		breq1	$⊢ g = c \to (g \leq c \leftrightarrow c \leq c)$
129		fveq2	$⊢ g = c \to ldgIdlSeq (R) (a) (g) = ldgIdlSeq (R) (a) (c)$
130		fveq2	$⊢ g = c \to ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g) = ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c)$
131	129 130	sseq12d	$⊢ g = c \to (ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g) \leftrightarrow ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c))$
132	128 131	imbi12d	$⊢ g = c \to ((g \leq c \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)) \leftrightarrow (c \leq c \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c)))$
133	132	rspcva	$⊢ (c \in ℕ_{0} \land \forall g \in ℕ_{0} (g \leq c \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g))) \to (c \leq c \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c))$
134	75 127 133	syl2anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to (c \leq c \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c))$
135	125 134	mpd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c)$
136	135	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c)$
137	67	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to R \in Ring$
138	70	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to RSpan (P) (⋃ ran f) \in LIdeal (P)$
139	75	adantr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to c \in ℕ_{0}$
140		simprl	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to g \in ℕ_{0}$
141		simprr	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to c \leq g$
142	1 10 11 137 138 139 140 141	hbtlem4	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
143	136 142	sstrd	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to ldgIdlSeq (R) (a) (c) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
144	123 143	eqsstrd	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land (g \in ℕ_{0} \land c \leq g)) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
145	144	anassrs	$⊢ (((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \land c \leq g) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
146	74 77 110 145	lecasei	$⊢ ((((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \land g \in ℕ_{0}) \to ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
147	146	ralrimiva	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to \forall g \in ℕ_{0} ldgIdlSeq (R) (a) (g) \subseteq ldgIdlSeq (R) (RSpan (P) (⋃ ran f)) (g)$
148	1 10 11 67 70 47 72 147	hbtlem5	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to RSpan (P) (⋃ ran f) = a$
149	148	eqcomd	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to a = RSpan (P) (⋃ ran f)$
150		fveq2	$⊢ b = ⋃ ran f \to RSpan (P) (b) = RSpan (P) (⋃ ran f)$
151	150	rspceeqv	$⊢ (⋃ ran f \in (𝒫 {Base}_{P} \cap Fin) \land a = RSpan (P) (⋃ ran f)) \to \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b)$
152	66 149 151	syl2anc	$⊢ (((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \land (f : (0 \dots c) ⟶ 𝒫 a \cap Fin \land \forall e \in (0 \dots c) ldgIdlSeq (R) (a) (e) \subseteq ldgIdlSeq (R) (RSpan (P) (f (e))) (e))) \to \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b)$
153	39 152	exlimddv	$⊢ ((R \in LNoeR \land a \in LIdeal (P)) \land (c \in ℕ_{0} \land \forall d \in ℤ_{\geq c} ldgIdlSeq (R) (a) (d) = ldgIdlSeq (R) (a) (c))) \to \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b)$
154	25 153	rexlimddv	$⊢ (R \in LNoeR \land a \in LIdeal (P)) \to \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b)$
155	154	ralrimiva	$⊢ R \in LNoeR \to \forall a \in LIdeal (P) \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b)$
156	48 10 27	islnr2	$⊢ P \in LNoeR \leftrightarrow (P \in Ring \land \forall a \in LIdeal (P) \exists b \in (𝒫 {Base}_{P} \cap Fin) a = RSpan (P) (b))$
157	4 155 156	sylanbrc	$⊢ R \in LNoeR \to P \in LNoeR$

Metamath Proof Explorer

Theorem hbt

Proof