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 = Poly 1 R
Assertion hbt R LNoeR P LNoeR

Proof

Step Hyp Ref Expression
1 hbt.p P = Poly 1 R
2 lnrring R LNoeR R Ring
3 1 ply1ring R Ring P Ring
4 2 3 syl R LNoeR P Ring
5 eqid Base R = Base R
6 eqid LIdeal R = LIdeal R
7 5 6 islnr3 R LNoeR R Ring LIdeal R NoeACS Base R
8 7 simprbi R LNoeR LIdeal R NoeACS Base R
9 8 adantr R LNoeR a LIdeal P LIdeal R NoeACS Base R
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 0 ldgIdlSeq R a b ldgIdlSeq R a b + 1
24 nacsfix LIdeal R NoeACS Base R ldgIdlSeq R a : 0 LIdeal R b 0 ldgIdlSeq R a b ldgIdlSeq R a b + 1 c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c
25 9 13 23 24 syl3anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq 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 Fin ldgIdlSeq R a e ldgIdlSeq R RSpan P b e
33 32 ralrimiva R LNoeR a LIdeal P e 0 c b 𝒫 a Fin ldgIdlSeq 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 Fin ldgIdlSeq R a e ldgIdlSeq R RSpan P b e f f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e
38 26 33 37 sylancr R LNoeR a LIdeal P f f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e
39 38 adantr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e ran f 𝒫 a
44 43 unissd R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e ran f a
47 simpllr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e a LIdeal P
48 eqid Base P = Base P
49 48 10 lidlss a LIdeal P a Base P
50 47 49 syl R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e a Base P
51 46 50 sstrd R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e ran f Base P
52 fvex Base P V
53 52 elpw2 ran f 𝒫 Base P ran f Base P
54 51 53 sylibr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e ran f 𝒫 Base P
55 simprl R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e f : 0 c 𝒫 a Fin
56 ffn f : 0 c 𝒫 a Fin f Fn 0 c
57 fniunfv f Fn 0 c g = 0 c f g = ran f
58 55 56 57 3syl R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g = 0 c f g = ran f
59 inss2 𝒫 a Fin Fin
60 55 ffvelrnda R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 c f g 𝒫 a Fin
61 59 60 sseldi R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 c f g Fin
63 iunfi 0 c Fin g 0 c f g Fin g = 0 c f g Fin
64 26 62 63 sylancr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g = 0 c f g Fin
65 58 64 eqeltrrd R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e ran f 𝒫 Base P Fin
67 2 ad3antrrr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e R Ring
68 4 ad3antrrr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e P Ring
69 27 48 10 rspcl P Ring ran f Base P RSpan P ran f LIdeal P
70 68 51 69 syl2anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 g
75 simplrl R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e c 0
76 75 adantr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 c
78 simprl R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 g c e 0 c ldgIdlSeq 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 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e f g Base P
96 27 48 10 rspcl P Ring f g Base P RSpan P f g LIdeal P
97 68 95 96 syl2anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e P Ring
101 100 adantr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 g c P Ring
102 27 48 rspssid P Ring ran f Base P ran f RSpan P ran f
103 68 51 102 syl2anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c d c ldgIdlSeq R a d = ldgIdlSeq R a c
120 119 ad2antrr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 c g d c ldgIdlSeq 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 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e c
125 124 leidd R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e c c
126 109 expr R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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
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 0 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
134 75 127 133 syl2anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e g 0 ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq 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 𝒫 Base P Fin a = RSpan P ran f b 𝒫 Base P Fin a = RSpan P b
152 66 149 151 syl2anc R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c f : 0 c 𝒫 a Fin e 0 c ldgIdlSeq R a e ldgIdlSeq R RSpan P f e e b 𝒫 Base P Fin a = RSpan P b
153 39 152 exlimddv R LNoeR a LIdeal P c 0 d c ldgIdlSeq R a d = ldgIdlSeq R a c b 𝒫 Base P Fin a = RSpan P b
154 25 153 rexlimddv R LNoeR a LIdeal P b 𝒫 Base P Fin a = RSpan P b
155 154 ralrimiva R LNoeR a LIdeal P b 𝒫 Base P Fin a = RSpan P b
156 48 10 27 islnr2 P LNoeR P Ring a LIdeal P b 𝒫 Base P Fin a = RSpan P b
157 4 155 156 sylanbrc R LNoeR P LNoeR