Users' Mathboxes 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 40004
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 𝑃 = (Poly1𝑅)
Assertion
Ref Expression
hbt (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR)

Proof of Theorem hbt
Dummy variables 𝑎 𝑏 𝑐 𝑒 𝑓 𝑔 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lnrring 39986 . . 3 (𝑅 ∈ LNoeR → 𝑅 ∈ Ring)
2 hbt.p . . . 4 𝑃 = (Poly1𝑅)
32ply1ring 20875 . . 3 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
41, 3syl 17 . 2 (𝑅 ∈ LNoeR → 𝑃 ∈ Ring)
5 eqid 2822 . . . . . . . 8 (Base‘𝑅) = (Base‘𝑅)
6 eqid 2822 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
75, 6islnr3 39989 . . . . . . 7 (𝑅 ∈ LNoeR ↔ (𝑅 ∈ Ring ∧ (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅))))
87simprbi 500 . . . . . 6 (𝑅 ∈ LNoeR → (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)))
98adantr 484 . . . . 5 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → (LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)))
10 eqid 2822 . . . . . . 7 (LIdeal‘𝑃) = (LIdeal‘𝑃)
11 eqid 2822 . . . . . . 7 (ldgIdlSeq‘𝑅) = (ldgIdlSeq‘𝑅)
122, 10, 11, 6hbtlem7 39999 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅))
131, 12sylan 583 . . . . 5 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅))
141ad2antrr 725 . . . . . . 7 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑅 ∈ Ring)
15 simplr 768 . . . . . . 7 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑎 ∈ (LIdeal‘𝑃))
16 simpr 488 . . . . . . 7 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑏 ∈ ℕ0)
17 peano2nn0 11925 . . . . . . . 8 (𝑏 ∈ ℕ0 → (𝑏 + 1) ∈ ℕ0)
1817adantl 485 . . . . . . 7 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → (𝑏 + 1) ∈ ℕ0)
19 nn0re 11894 . . . . . . . . 9 (𝑏 ∈ ℕ0𝑏 ∈ ℝ)
2019lep1d 11560 . . . . . . . 8 (𝑏 ∈ ℕ0𝑏 ≤ (𝑏 + 1))
2120adantl 485 . . . . . . 7 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑏 ≤ (𝑏 + 1))
222, 10, 11, 14, 15, 16, 18, 21hbtlem4 40000 . . . . . 6 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1)))
2322ralrimiva 3174 . . . . 5 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑏 ∈ ℕ0 (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1)))
24 nacsfix 39583 . . . . 5 (((LIdeal‘𝑅) ∈ (NoeACS‘(Base‘𝑅)) ∧ ((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅) ∧ ∀𝑏 ∈ ℕ0 (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1))) → ∃𝑐 ∈ ℕ0𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
259, 13, 23, 24syl3anc 1368 . . . 4 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑐 ∈ ℕ0𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
26 fzfi 13335 . . . . . . 7 (0...𝑐) ∈ Fin
27 eqid 2822 . . . . . . . . 9 (RSpan‘𝑃) = (RSpan‘𝑃)
28 simpll 766 . . . . . . . . 9 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑅 ∈ LNoeR)
29 simplr 768 . . . . . . . . 9 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑎 ∈ (LIdeal‘𝑃))
30 elfznn0 12995 . . . . . . . . . 10 (𝑒 ∈ (0...𝑐) → 𝑒 ∈ ℕ0)
3130adantl 485 . . . . . . . . 9 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑒 ∈ ℕ0)
322, 10, 11, 27, 28, 29, 31hbtlem6 40003 . . . . . . . 8 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒))
3332ralrimiva 3174 . . . . . . 7 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑒 ∈ (0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒))
34 2fveq3 6657 . . . . . . . . . 10 (𝑏 = (𝑓𝑒) → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏)) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒))))
3534fveq1d 6654 . . . . . . . . 9 (𝑏 = (𝑓𝑒) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))
3635sseq2d 3974 . . . . . . . 8 (𝑏 = (𝑓𝑒) → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒)))
3736ac6sfi 8750 . . . . . . 7 (((0...𝑐) ∈ Fin ∧ ∀𝑒 ∈ (0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒)))
3826, 33, 37sylancr 590 . . . . . 6 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒)))
3938adantr 484 . . . . 5 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒)))
40 frn 6500 . . . . . . . . . . . . 13 (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin))
4140ad2antrl 727 . . . . . . . . . . . 12 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin))
42 inss1 4179 . . . . . . . . . . . 12 (𝒫 𝑎 ∩ Fin) ⊆ 𝒫 𝑎
4341, 42sstrdi 3954 . . . . . . . . . . 11 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ⊆ 𝒫 𝑎)
4443unissd 4823 . . . . . . . . . 10 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 𝒫 𝑎)
45 unipw 5320 . . . . . . . . . 10 𝒫 𝑎 = 𝑎
4644, 45sseqtrdi 3992 . . . . . . . . 9 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓𝑎)
47 simpllr 775 . . . . . . . . . 10 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑎 ∈ (LIdeal‘𝑃))
48 eqid 2822 . . . . . . . . . . 11 (Base‘𝑃) = (Base‘𝑃)
4948, 10lidlss 19974 . . . . . . . . . 10 (𝑎 ∈ (LIdeal‘𝑃) → 𝑎 ⊆ (Base‘𝑃))
5047, 49syl 17 . . . . . . . . 9 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑎 ⊆ (Base‘𝑃))
5146, 50sstrd 3952 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ⊆ (Base‘𝑃))
52 fvex 6665 . . . . . . . . 9 (Base‘𝑃) ∈ V
5352elpw2 5224 . . . . . . . 8 ( ran 𝑓 ∈ 𝒫 (Base‘𝑃) ↔ ran 𝑓 ⊆ (Base‘𝑃))
5451, 53sylibr 237 . . . . . . 7 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ∈ 𝒫 (Base‘𝑃))
55 simprl 770 . . . . . . . . 9 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin))
56 ffn 6494 . . . . . . . . 9 (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → 𝑓 Fn (0...𝑐))
57 fniunfv 6989 . . . . . . . . 9 (𝑓 Fn (0...𝑐) → 𝑔 ∈ (0...𝑐)(𝑓𝑔) = ran 𝑓)
5855, 56, 573syl 18 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑔 ∈ (0...𝑐)(𝑓𝑔) = ran 𝑓)
59 inss2 4180 . . . . . . . . . . 11 (𝒫 𝑎 ∩ Fin) ⊆ Fin
6055ffvelrnda 6833 . . . . . . . . . . 11 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓𝑔) ∈ (𝒫 𝑎 ∩ Fin))
6159, 60sseldi 3940 . . . . . . . . . 10 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓𝑔) ∈ Fin)
6261ralrimiva 3174 . . . . . . . . 9 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ∀𝑔 ∈ (0...𝑐)(𝑓𝑔) ∈ Fin)
63 iunfi 8800 . . . . . . . . 9 (((0...𝑐) ∈ Fin ∧ ∀𝑔 ∈ (0...𝑐)(𝑓𝑔) ∈ Fin) → 𝑔 ∈ (0...𝑐)(𝑓𝑔) ∈ Fin)
6426, 62, 63sylancr 590 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑔 ∈ (0...𝑐)(𝑓𝑔) ∈ Fin)
6558, 64eqeltrrd 2915 . . . . . . 7 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ∈ Fin)
6654, 65elind 4145 . . . . . 6 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ∈ (𝒫 (Base‘𝑃) ∩ Fin))
671ad3antrrr 729 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑅 ∈ Ring)
684ad3antrrr 729 . . . . . . . . 9 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑃 ∈ Ring)
6927, 48, 10rspcl 19986 . . . . . . . . 9 ((𝑃 ∈ Ring ∧ ran 𝑓 ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘ ran 𝑓) ∈ (LIdeal‘𝑃))
7068, 51, 69syl2anc 587 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘ ran 𝑓) ∈ (LIdeal‘𝑃))
7127, 10rspssp 19990 . . . . . . . . 9 ((𝑃 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃) ∧ ran 𝑓𝑎) → ((RSpan‘𝑃)‘ ran 𝑓) ⊆ 𝑎)
7268, 47, 46, 71syl3anc 1368 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘ ran 𝑓) ⊆ 𝑎)
73 nn0re 11894 . . . . . . . . . . 11 (𝑔 ∈ ℕ0𝑔 ∈ ℝ)
7473adantl 485 . . . . . . . . . 10 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑔 ∈ ℝ)
75 simplrl 776 . . . . . . . . . . . 12 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑐 ∈ ℕ0)
7675adantr 484 . . . . . . . . . . 11 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑐 ∈ ℕ0)
7776nn0red 11944 . . . . . . . . . 10 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑐 ∈ ℝ)
78 simprl 770 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑔 ∈ ℕ0)
79 simprr 772 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑔𝑐)
8075adantr 484 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑐 ∈ ℕ0)
81 fznn0 12994 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℕ0 → (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ0𝑔𝑐)))
8280, 81syl 17 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ0𝑔𝑐)))
8378, 79, 82mpbir2and 712 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑔 ∈ (0...𝑐))
84 simplrr 777 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))
85 fveq2 6652 . . . . . . . . . . . . . . 15 (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔))
86 2fveq3 6657 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑔 → ((RSpan‘𝑃)‘(𝑓𝑒)) = ((RSpan‘𝑃)‘(𝑓𝑔)))
8786fveq2d 6656 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑔 → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒))) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔))))
88 id 22 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑔𝑒 = 𝑔)
8987, 88fveq12d 6659 . . . . . . . . . . . . . . 15 (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔)))‘𝑔))
9085, 89sseq12d 3975 . . . . . . . . . . . . . 14 (𝑒 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔)))‘𝑔)))
9190rspcva 3596 . . . . . . . . . . . . 13 ((𝑔 ∈ (0...𝑐) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔)))‘𝑔))
9283, 84, 91syl2anc 587 . . . . . . . . . . . 12 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔)))‘𝑔))
9367adantr 484 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑅 ∈ Ring)
94 fvssunirn 6681 . . . . . . . . . . . . . . . 16 (𝑓𝑔) ⊆ ran 𝑓
9594, 51sstrid 3953 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → (𝑓𝑔) ⊆ (Base‘𝑃))
9627, 48, 10rspcl 19986 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Ring ∧ (𝑓𝑔) ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘(𝑓𝑔)) ∈ (LIdeal‘𝑃))
9768, 95, 96syl2anc 587 . . . . . . . . . . . . . 14 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘(𝑓𝑔)) ∈ (LIdeal‘𝑃))
9897adantr 484 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → ((RSpan‘𝑃)‘(𝑓𝑔)) ∈ (LIdeal‘𝑃))
9970adantr 484 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → ((RSpan‘𝑃)‘ ran 𝑓) ∈ (LIdeal‘𝑃))
10067, 3syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑃 ∈ Ring)
101100adantr 484 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → 𝑃 ∈ Ring)
10227, 48rspssid 19987 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Ring ∧ ran 𝑓 ⊆ (Base‘𝑃)) → ran 𝑓 ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
10368, 51, 102syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ran 𝑓 ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
104103adantr 484 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → ran 𝑓 ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
10594, 104sstrid 3953 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → (𝑓𝑔) ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
10627, 10rspssp 19990 . . . . . . . . . . . . . 14 ((𝑃 ∈ Ring ∧ ((RSpan‘𝑃)‘ ran 𝑓) ∈ (LIdeal‘𝑃) ∧ (𝑓𝑔) ⊆ ((RSpan‘𝑃)‘ ran 𝑓)) → ((RSpan‘𝑃)‘(𝑓𝑔)) ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
107101, 99, 105, 106syl3anc 1368 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → ((RSpan‘𝑃)‘(𝑓𝑔)) ⊆ ((RSpan‘𝑃)‘ ran 𝑓))
1082, 10, 11, 93, 98, 99, 107, 78hbtlem3 40001 . . . . . . . . . . . 12 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑔)))‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
10992, 108sstrd 3952 . . . . . . . . . . 11 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑔𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
110109anassrs 471 . . . . . . . . . 10 ((((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) ∧ 𝑔𝑐) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
111 nn0z 11993 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℕ0𝑐 ∈ ℤ)
112111adantr 484 . . . . . . . . . . . . . . 15 ((𝑐 ∈ ℕ0 ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑐 ∈ ℤ)
113 nn0z 11993 . . . . . . . . . . . . . . . 16 (𝑔 ∈ ℕ0𝑔 ∈ ℤ)
114113ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝑐 ∈ ℕ0 ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑔 ∈ ℤ)
115 simprr 772 . . . . . . . . . . . . . . 15 ((𝑐 ∈ ℕ0 ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑐𝑔)
116 eluz2 12237 . . . . . . . . . . . . . . 15 (𝑔 ∈ (ℤ𝑐) ↔ (𝑐 ∈ ℤ ∧ 𝑔 ∈ ℤ ∧ 𝑐𝑔))
117112, 114, 115, 116syl3anbrc 1340 . . . . . . . . . . . . . 14 ((𝑐 ∈ ℕ0 ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑔 ∈ (ℤ𝑐))
11875, 117sylan 583 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑔 ∈ (ℤ𝑐))
119 simprr 772 . . . . . . . . . . . . . 14 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
120119ad2antrr 725 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
121 fveqeq2 6661 . . . . . . . . . . . . . 14 (𝑑 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)))
122121rspcva 3596 . . . . . . . . . . . . 13 ((𝑔 ∈ (ℤ𝑐) ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
123118, 120, 122syl2anc 587 . . . . . . . . . . . 12 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
12475nn0red 11944 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑐 ∈ ℝ)
125124leidd 11195 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑐𝑐)
126109expr 460 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → (𝑔𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔)))
127126ralrimiva 3174 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ0 (𝑔𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔)))
128 breq1 5045 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑐 → (𝑔𝑐𝑐𝑐))
129 fveq2 6652 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))
130 fveq2 6652 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐))
131129, 130sseq12d 3975 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑐 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐)))
132128, 131imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑐 → ((𝑔𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔)) ↔ (𝑐𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐))))
133132rspcva 3596 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ ℕ0 ∧ ∀𝑔 ∈ ℕ0 (𝑔𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))) → (𝑐𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐)))
13475, 127, 133syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → (𝑐𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐)))
135125, 134mpd 15 . . . . . . . . . . . . . 14 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐))
136135adantr 484 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐))
13767adantr 484 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑅 ∈ Ring)
13870adantr 484 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → ((RSpan‘𝑃)‘ ran 𝑓) ∈ (LIdeal‘𝑃))
13975adantr 484 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑐 ∈ ℕ0)
140 simprl 770 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑔 ∈ ℕ0)
141 simprr 772 . . . . . . . . . . . . . 14 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → 𝑐𝑔)
1422, 10, 11, 137, 138, 139, 140, 141hbtlem4 40000 . . . . . . . . . . . . 13 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
143136, 142sstrd 3952 . . . . . . . . . . . 12 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
144123, 143eqsstrd 3980 . . . . . . . . . . 11 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0𝑐𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
145144anassrs 471 . . . . . . . . . 10 ((((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) ∧ 𝑐𝑔) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
14674, 77, 110, 145lecasei 10735 . . . . . . . . 9 (((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
147146ralrimiva 3174 . . . . . . . 8 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ0 (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘ ran 𝑓))‘𝑔))
1482, 10, 11, 67, 70, 47, 72, 147hbtlem5 40002 . . . . . . 7 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘ ran 𝑓) = 𝑎)
149148eqcomd 2828 . . . . . 6 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → 𝑎 = ((RSpan‘𝑃)‘ ran 𝑓))
150 fveq2 6652 . . . . . . 7 (𝑏 = ran 𝑓 → ((RSpan‘𝑃)‘𝑏) = ((RSpan‘𝑃)‘ ran 𝑓))
151150rspceeqv 3613 . . . . . 6 (( ran 𝑓 ∈ (𝒫 (Base‘𝑃) ∩ Fin) ∧ 𝑎 = ((RSpan‘𝑃)‘ ran 𝑓)) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
15266, 149, 151syl2anc 587 . . . . 5 ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓𝑒)))‘𝑒))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
15339, 152exlimddv 1936 . . . 4 (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧ ∀𝑑 ∈ (ℤ𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
15425, 153rexlimddv 3277 . . 3 ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
155154ralrimiva 3174 . 2 (𝑅 ∈ LNoeR → ∀𝑎 ∈ (LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))
15648, 10, 27islnr2 39988 . 2 (𝑃 ∈ LNoeR ↔ (𝑃 ∈ Ring ∧ ∀𝑎 ∈ (LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)))
1574, 155, 156sylanbrc 586 1 (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2114  wral 3130  wrex 3131  cin 3907  wss 3908  𝒫 cpw 4511   cuni 4813   ciun 4894   class class class wbr 5042  ran crn 5533   Fn wfn 6329  wf 6330  cfv 6334  (class class class)co 7140  Fincfn 8496  cr 10525  0cc0 10526  1c1 10527   + caddc 10529  cle 10665  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  Basecbs 16474  Ringcrg 19288  LIdealclidl 19933  RSpancrsp 19934  Poly1cpl1 20804  NoeACScnacs 39573  LNoeRclnr 39983  ldgIdlSeqcldgis 39995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-ofr 7395  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ocomp 16577  df-ds 16578  df-unif 16579  df-0g 16706  df-gsum 16707  df-mre 16848  df-mrc 16849  df-acs 16851  df-proset 17529  df-drs 17530  df-poset 17547  df-ipo 17753  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-mhm 17947  df-submnd 17948  df-grp 18097  df-minusg 18098  df-sbg 18099  df-mulg 18216  df-subg 18267  df-ghm 18347  df-cntz 18438  df-cmn 18899  df-abl 18900  df-mgp 19231  df-ur 19243  df-ring 19290  df-cring 19291  df-oppr 19367  df-dvdsr 19385  df-unit 19386  df-invr 19416  df-subrg 19524  df-lmod 19627  df-lss 19695  df-lsp 19735  df-sra 19935  df-rgmod 19936  df-lidl 19937  df-rsp 19938  df-rlreg 20047  df-cnfld 20090  df-ascl 20542  df-psr 20592  df-mvr 20593  df-mpl 20594  df-opsr 20596  df-psr1 20807  df-vr1 20808  df-ply1 20809  df-coe1 20810  df-mdeg 24654  df-deg1 24655  df-nacs 39574  df-lfig 39942  df-lnm 39950  df-lnr 39984  df-ldgis 39996
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator