Metamath Proof Explorer

Theorem 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=Poly1⁡R
Assertion hbt ⊢R∈LNoeR→P∈LNoeR

Proof

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