hbt - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hbt		Structured version Visualization version GIF version

Theorem hbt 36719

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.)

**Hypothesis**
Ref	Expression
hbt.p	⊢ 𝑃 = (Poly₁‘𝑅)

**Assertion**
Ref	Expression
hbt	⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR)

Proof of Theorem hbt Dummy variables 𝑎 𝑏 𝑐 𝑒 𝑓 𝑔 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lnrring 36701	. . 3 ⊢ (𝑅 ∈ LNoeR → 𝑅 ∈ Ring)
2		hbt.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
3	2	ply1ring 19439	. . 3 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
4	1, 3	syl 17	. 2 ⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ Ring)
5		eqid 2610	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
6		eqid 2610	. . . . . . . 8 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
7	5, 6	islnr3 36704	. . . . . . 7 ⊢ (𝑅 ∈ LNoeR ↔ (𝑅 ∈ Ring ∧ (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅))))
8	7	simprbi 479	. . . . . 6 ⊢ (𝑅 ∈ LNoeR → (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)))
9	8	adantr 480	. . . . 5 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)))
10		eqid 2610	. . . . . . 7 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
11		eqid 2610	. . . . . . 7 ⊢ (ldgIdlSeq‘𝑅) = (ldgIdlSeq‘𝑅)
12	2, 10, 11, 6	hbtlem7 36714	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ((ldgIdlSeq‘𝑅)‘𝑎):ℕ₀⟶(LIdeal‘𝑅))
13	1, 12	sylan 487	. . . . 5 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ((ldgIdlSeq‘𝑅)‘𝑎):ℕ₀⟶(LIdeal‘𝑅))
14	1	ad2antrr 758	. . . . . . 7 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → 𝑅 ∈ Ring)
15		simplr 788	. . . . . . 7 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → 𝑎 ∈ (LIdeal‘𝑃))
16		simpr 476	. . . . . . 7 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → 𝑏 ∈ ℕ₀)
17		peano2nn0 11210	. . . . . . . 8 ⊢ (𝑏 ∈ ℕ₀ → (𝑏 + 1) ∈ ℕ₀)
18	17	adantl 481	. . . . . . 7 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → (𝑏 + 1) ∈ ℕ₀)
19		nn0re 11178	. . . . . . . . 9 ⊢ (𝑏 ∈ ℕ₀ → 𝑏 ∈ ℝ)
20	19	lep1d 10834	. . . . . . . 8 ⊢ (𝑏 ∈ ℕ₀ → 𝑏 ≤ (𝑏 + 1))
21	20	adantl 481	. . . . . . 7 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → 𝑏 ≤ (𝑏 + 1))
22	2, 10, 11, 14, 15, 16, 18, 21	hbtlem4 36715	. . . . . 6 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ₀) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1)))
23	22	ralrimiva 2949	. . . . 5 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑏 ∈ ℕ₀ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1)))
24		nacsfix 36293	. . . . 5 ⊢ (((LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)) ∧ ((ldgIdlSeq‘𝑅)‘𝑎):ℕ₀⟶(LIdeal‘𝑅) ∧ ∀𝑏 ∈ ℕ₀ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1))) → ∃𝑐 ∈ ℕ₀ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
25	9, 13, 23, 24	syl3anc 1318	. . . 4 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑐 ∈ ℕ₀ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
26		fzfi 12633	. . . . . . 7 ⊢ (0...𝑐) ∈ Fin
27		eqid 2610	. . . . . . . . 9 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
28		simpll 786	. . . . . . . . 9 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑅 ∈ LNoeR)
29		simplr 788	. . . . . . . . 9 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑎 ∈ (LIdeal‘𝑃))
30		elfznn0 12302	. . . . . . . . . 10 ⊢ (𝑒 ∈ (0...𝑐) → 𝑒 ∈ ℕ₀)
31	30	adantl 481	. . . . . . . . 9 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑒 ∈ ℕ₀)
32	2, 10, 11, 27, 28, 29, 31	hbtlem6 36718	. . . . . . . 8 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒))
33	32	ralrimiva 2949	. . . . . . 7 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑒 ∈ (0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒))
34		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑓‘𝑒) → ((RSpan‘𝑃)‘𝑏) = ((RSpan‘𝑃)‘(𝑓‘𝑒)))
35	34	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑏 = (𝑓‘𝑒) → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏)) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒))))
36	35	fveq1d 6105	. . . . . . . . 9 ⊢ (𝑏 = (𝑓‘𝑒) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))
37	36	sseq2d 3596	. . . . . . . 8 ⊢ (𝑏 = (𝑓‘𝑒) → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)))
38	37	ac6sfi 8089	. . . . . . 7 ⊢ (((0...𝑐) ∈ Fin ∧ ∀𝑒 ∈ (0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)))
39	26, 33, 38	sylancr 694	. . . . . 6 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)))
40	39	adantr 480	. . . . 5 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)))
41		frn 5966	. . . . . . . . . . . . 13 ⊢ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin))
42	41	ad2antrl 760	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin))
43		inss1 3795	. . . . . . . . . . . 12 ⊢ (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
44	42, 43	syl6ss 3580	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ran 𝑓 ⊆ 𝒫 𝑎)
45	44	unissd 4398	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ⊆ ∪ 𝒫 𝑎)
46		unipw 4845	. . . . . . . . . 10 ⊢ ∪ 𝒫 𝑎 = 𝑎
47	45, 46	syl6sseq 3614	. . . . . . . . 9 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ⊆ 𝑎)
48		simpllr 795	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 ∈ (LIdeal‘𝑃))
49		eqid 2610	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘𝑃)
50	49, 10	lidlss 19031	. . . . . . . . . 10 ⊢ (𝑎 ∈ (LIdeal‘𝑃) → 𝑎 ⊆ (Base‘𝑃))
51	48, 50	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 ⊆ (Base‘𝑃))
52	47, 51	sstrd 3578	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ⊆ (Base‘𝑃))
53		fvex 6113	. . . . . . . . 9 ⊢ (Base‘𝑃) ∈ V
54	53	elpw2 4755	. . . . . . . 8 ⊢ (∪ ran 𝑓 ∈ 𝒫 (Base‘𝑃) ↔ ∪ ran 𝑓 ⊆ (Base‘𝑃))
55	52, 54	sylibr 223	. . . . . . 7 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ∈ 𝒫 (Base‘𝑃))
56		simprl 790	. . . . . . . . 9 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin))
57		ffn 5958	. . . . . . . . 9 ⊢ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → 𝑓 Fn (0...𝑐))
58		fniunfv 6409	. . . . . . . . 9 ⊢ (𝑓 Fn (0...𝑐) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) = ∪ ran 𝑓)
59	56, 57, 58	3syl 18	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) = ∪ ran 𝑓)
60		inss2 3796	. . . . . . . . . . 11 ⊢ (𝒫 𝑎 ∩ Fin) ⊆ Fin
61	56	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓‘𝑔) ∈ (𝒫 𝑎 ∩ Fin))
62	60, 61	sseldi 3566	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓‘𝑔) ∈ Fin)
63	62	ralrimiva 2949	. . . . . . . . 9 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin)
64		iunfi 8137	. . . . . . . . 9 ⊢ (((0...𝑐) ∈ Fin ∧ ∀𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin)
65	26, 63, 64	sylancr 694	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin)
66	59, 65	eqeltrrd 2689	. . . . . . 7 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ∈ Fin)
67	55, 66	elind 3760	. . . . . 6 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ∈ (𝒫 (Base‘𝑃) ∩ Fin))
68	1	ad3antrrr 762	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑅 ∈ Ring)
69	4	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑃 ∈ Ring)
70	27, 49, 10	rspcl 19043	. . . . . . . . 9 ⊢ ((𝑃 ∈ Ring ∧ ∪ ran 𝑓 ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘∪ ran 𝑓) ∈ (LIdeal‘𝑃))
71	69, 52, 70	syl2anc 691	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran 𝑓) ∈ (LIdeal‘𝑃))
72	27, 10	rspssp 19047	. . . . . . . . 9 ⊢ ((𝑃 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃) ∧ ∪ ran 𝑓 ⊆ 𝑎) → ((RSpan‘𝑃)‘∪ ran 𝑓) ⊆ 𝑎)
73	69, 48, 47, 72	syl3anc 1318	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran 𝑓) ⊆ 𝑎)
74		nn0re 11178	. . . . . . . . . . 11 ⊢ (𝑔 ∈ ℕ₀ → 𝑔 ∈ ℝ)
75	74	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) → 𝑔 ∈ ℝ)
76		simplrl 796	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ∈ ℕ₀)
77	76	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) → 𝑐 ∈ ℕ₀)
78	77	nn0red 11229	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) → 𝑐 ∈ ℝ)
79		simprl 790	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑔 ∈ ℕ₀)
80		simprr 792	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑔 ≤ 𝑐)
81	76	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑐 ∈ ℕ₀)
82		fznn0 12301	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ℕ₀ → (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)))
83	81, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)))
84	79, 80, 83	mpbir2and 959	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑔 ∈ (0...𝑐))
85		simplrr 797	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))
86		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔))
87		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑔 → (𝑓‘𝑒) = (𝑓‘𝑔))
88	87	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑔 → ((RSpan‘𝑃)‘(𝑓‘𝑒)) = ((RSpan‘𝑃)‘(𝑓‘𝑔)))
89	88	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑔 → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒))) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔))))
90		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑔 → 𝑒 = 𝑔)
91	89, 90	fveq12d 6109	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔))
92	86, 91	sseq12d 3597	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔)))
93	92	rspcva 3280	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ (0...𝑐) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔))
94	84, 85, 93	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔))
95	68	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑅 ∈ Ring)
96		fvssunirn 6127	. . . . . . . . . . . . . . . 16 ⊢ (𝑓‘𝑔) ⊆ ∪ ran 𝑓
97	96, 52	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (𝑓‘𝑔) ⊆ (Base‘𝑃))
98	27, 49, 10	rspcl 19043	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ Ring ∧ (𝑓‘𝑔) ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃))
99	69, 97, 98	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃))
100	99	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃))
101	71	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘∪ ran 𝑓) ∈ (LIdeal‘𝑃))
102	68, 3	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑃 ∈ Ring)
103	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → 𝑃 ∈ Ring)
104	27, 49	rspssid 19044	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ ∪ ran 𝑓 ⊆ (Base‘𝑃)) → ∪ ran 𝑓 ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
105	69, 52, 104	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran 𝑓 ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
106	105	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → ∪ ran 𝑓 ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
107	96, 106	syl5ss 3579	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → (𝑓‘𝑔) ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
108	27, 10	rspssp 19047	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ Ring ∧ ((RSpan‘𝑃)‘∪ ran 𝑓) ∈ (LIdeal‘𝑃) ∧ (𝑓‘𝑔) ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
109	103, 101, 107, 108	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ⊆ ((RSpan‘𝑃)‘∪ ran 𝑓))
110	2, 10, 11, 95, 100, 101, 109, 79	hbtlem3 36716	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
111	94, 110	sstrd 3578	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
112	111	anassrs 678	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) ∧ 𝑔 ≤ 𝑐) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
113		nn0z 11277	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ ℕ₀ → 𝑐 ∈ ℤ)
114	113	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ ℕ₀ ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑐 ∈ ℤ)
115		nn0z 11277	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ ℕ₀ → 𝑔 ∈ ℤ)
116	115	ad2antrl 760	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ ℕ₀ ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ ℤ)
117		simprr 792	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ ℕ₀ ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑐 ≤ 𝑔)
118		eluz2 11569	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ (ℤ_≥‘𝑐) ↔ (𝑐 ∈ ℤ ∧ 𝑔 ∈ ℤ ∧ 𝑐 ≤ 𝑔))
119	114, 116, 117, 118	syl3anbrc 1239	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ℕ₀ ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ (ℤ_≥‘𝑐))
120	76, 119	sylan 487	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ (ℤ_≥‘𝑐))
121		simprr 792	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
122	121	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
123		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑔 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔))
124	123	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)))
125	124	rspcva 3280	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ (ℤ_≥‘𝑐) ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
126	120, 122, 125	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
127	76	nn0red 11229	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ∈ ℝ)
128	127	leidd 10473	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ≤ 𝑐)
129	111	expr 641	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) → (𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)))
130	129	ralrimiva 2949	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ₀ (𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)))
131		breq1 4586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑐 → (𝑔 ≤ 𝑐 ↔ 𝑐 ≤ 𝑐))
132		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
133		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))
134	132, 133	sseq12d 3597	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑐 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)))
135	131, 134	imbi12d 333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑐 → ((𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) ↔ (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))))
136	135	rspcva 3280	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ ℕ₀ ∧ ∀𝑔 ∈ ℕ₀ (𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))) → (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)))
137	76, 130, 136	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)))
138	128, 137	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))
139	138	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))
140	68	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑅 ∈ Ring)
141	71	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → ((RSpan‘𝑃)‘∪ ran 𝑓) ∈ (LIdeal‘𝑃))
142	76	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑐 ∈ ℕ₀)
143		simprl 790	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ ℕ₀)
144		simprr 792	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → 𝑐 ≤ 𝑔)
145	2, 10, 11, 140, 141, 142, 143, 144	hbtlem4 36715	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
146	139, 145	sstrd 3578	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
147	126, 146	eqsstrd 3602	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ₀ ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
148	147	anassrs 678	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) ∧ 𝑐 ≤ 𝑔) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
149	75, 78, 112, 148	lecasei 10022	. . . . . . . . 9 ⊢ (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ₀) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
150	149	ralrimiva 2949	. . . . . . . 8 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ₀ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))
151	2, 10, 11, 68, 71, 48, 73, 150	hbtlem5 36717	. . . . . . 7 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran 𝑓) = 𝑎)
152	151	eqcomd 2616	. . . . . 6 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 = ((RSpan‘𝑃)‘∪ ran 𝑓))
153		fveq2 6103	. . . . . . . 8 ⊢ (𝑏 = ∪ ran 𝑓 → ((RSpan‘𝑃)‘𝑏) = ((RSpan‘𝑃)‘∪ ran 𝑓))
154	153	eqeq2d 2620	. . . . . . 7 ⊢ (𝑏 = ∪ ran 𝑓 → (𝑎 = ((RSpan‘𝑃)‘𝑏) ↔ 𝑎 = ((RSpan‘𝑃)‘∪ ran 𝑓)))
155	154	rspcev 3282	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ (𝒫 (Base‘𝑃) ∩ Fin) ∧ 𝑎 = ((RSpan‘𝑃)‘∪ ran 𝑓)) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
156	67, 152, 155	syl2anc 691	. . . . 5 ⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
157	40, 156	exlimddv 1850	. . . 4 ⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ₀ ∧ ∀𝑑 ∈ (ℤ_≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
158	25, 157	rexlimddv 3017	. . 3 ⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
159	158	ralrimiva 2949	. 2 ⊢ (𝑅 ∈ LNoeR → ∀𝑎 ∈ (LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
160	49, 10, 27	islnr2 36703	. 2 ⊢ (𝑃 ∈ LNoeR ↔ (𝑃 ∈ Ring ∧ ∀𝑎 ∈ (LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)))
161	4, 159, 160	sylanbrc 695	1 ⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 ∩ cin 3539 ⊆ wss 3540 𝒫 cpw 4108 ∪ cuni 4372 ∪ ciun 4455 class class class wbr 4583 ran crn 5039 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 ≤ cle 9954 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 Basecbs 15695 Ringcrg 18370 LIdealclidl 18991 RSpancrsp 18992 Poly₁cpl1 19368 NoeACScnacs 36283 LNoeRclnr 36698 ldgIdlSeqcldgis 36710

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-ofr 6796 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-tpos 7239 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-sup 8231 df-oi 8298 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-fz 12198 df-fzo 12335 df-seq 12664 df-hash 12980 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ocomp 15790 df-ds 15791 df-unif 15792 df-0g 15925 df-gsum 15926 df-mre 16069 df-mrc 16070 df-acs 16072 df-preset 16751 df-drs 16752 df-poset 16769 df-ipo 16975 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-mhm 17158 df-submnd 17159 df-grp 17248 df-minusg 17249 df-sbg 17250 df-mulg 17364 df-subg 17414 df-ghm 17481 df-cntz 17573 df-cmn 18018 df-abl 18019 df-mgp 18313 df-ur 18325 df-ring 18372 df-cring 18373 df-oppr 18446 df-dvdsr 18464 df-unit 18465 df-invr 18495 df-subrg 18601 df-lmod 18688 df-lss 18754 df-lsp 18793 df-sra 18993 df-rgmod 18994 df-lidl 18995 df-rsp 18996 df-rlreg 19104 df-ascl 19135 df-psr 19177 df-mvr 19178 df-mpl 19179 df-opsr 19181 df-psr1 19371 df-vr1 19372 df-ply1 19373 df-coe1 19374 df-cnfld 19568 df-mdeg 23619 df-deg1 23620 df-nacs 36284 df-lfig 36656 df-lnm 36664 df-lnr 36699 df-ldgis 36711

This theorem is referenced by: (None)

W3C validator