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

Theorem hbt 29159
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
Assertion
Ref Expression
hbt

Proof of Theorem hbt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lnrrng 29141 . . 3
2 hbt.p . . . 4
32ply1rng 17467 . . 3
41, 3syl 16 . 2
5 eqid 2422 . . . . . . . 8
6 eqid 2422 . . . . . . . 8
75, 6islnr3 29144 . . . . . . 7
87simprbi 454 . . . . . 6
98adantr 455 . . . . 5
10 eqid 2422 . . . . . . 7
11 eqid 2422 . . . . . . 7
122, 10, 11, 6hbtlem7 29154 . . . . . 6
131, 12sylan 461 . . . . 5
141ad2antrr 710 . . . . . . 7
15 simplr 739 . . . . . . 7
16 simpr 451 . . . . . . 7
17 peano2nn0 10566 . . . . . . . 8
1817adantl 456 . . . . . . 7
19 nn0re 10534 . . . . . . . . 9
2019lep1d 10210 . . . . . . . 8
2120adantl 456 . . . . . . 7
222, 10, 11, 14, 15, 16, 18, 21hbtlem4 29155 . . . . . 6
2322ralrimiva 2778 . . . . 5
24 nacsfix 28720 . . . . 5
259, 13, 23, 24syl3anc 1203 . . . 4
26 fzfi 11735 . . . . . . 7
27 eqid 2422 . . . . . . . . 9
28 simpll 738 . . . . . . . . 9
29 simplr 739 . . . . . . . . 9
30 elfznn0 11425 . . . . . . . . . 10
3130adantl 456 . . . . . . . . 9
322, 10, 11, 27, 28, 29, 31hbtlem6 29158 . . . . . . . 8
3332ralrimiva 2778 . . . . . . 7
34 fveq2 5661 . . . . . . . . . . 11
3534fveq2d 5665 . . . . . . . . . 10
3635fveq1d 5663 . . . . . . . . 9
3736sseq2d 3361 . . . . . . . 8
3837ac6sfi 7515 . . . . . . 7
3926, 33, 38sylancr 648 . . . . . 6
4039adantr 455 . . . . 5
41 frn 5535 . . . . . . . . . . . . 13
4241ad2antrl 712 . . . . . . . . . . . 12
43 inss1 3547 . . . . . . . . . . . 12
4442, 43syl6ss 3345 . . . . . . . . . . 11
4544unissd 4090 . . . . . . . . . 10
46 unipw 4514 . . . . . . . . . 10
4745, 46syl6sseq 3379 . . . . . . . . 9
48 simpllr 743 . . . . . . . . . 10
49 eqid 2422 . . . . . . . . . . 11
5049, 10lidlss 17100 . . . . . . . . . 10
5148, 50syl 16 . . . . . . . . 9
5247, 51sstrd 3343 . . . . . . . 8
53 fvex 5671 . . . . . . . . 9
5453elpw2 4428 . . . . . . . 8
5552, 54sylibr 206 . . . . . . 7
56 simprl 740 . . . . . . . . 9
57 ffn 5529 . . . . . . . . 9
58 fniunfv 5932 . . . . . . . . 9
5956, 57, 583syl 19 . . . . . . . 8
60 inss2 3548 . . . . . . . . . . 11
6156ffvelrnda 5813 . . . . . . . . . . 11
6260, 61sseldi 3331 . . . . . . . . . 10
6362ralrimiva 2778 . . . . . . . . 9
64 iunfi 7558 . . . . . . . . 9
6526, 63, 64sylancr 648 . . . . . . . 8
6659, 65eqeltrrd 2497 . . . . . . 7
6755, 66elind 3517 . . . . . 6
681ad3antrrr 714 . . . . . . . 8
694ad3antrrr 714 . . . . . . . . 9
7027, 49, 10rspcl 17113 . . . . . . . . 9
7169, 52, 70syl2anc 646 . . . . . . . 8
7227, 10rspssp 17117 . . . . . . . . 9
7369, 48, 47, 72syl3anc 1203 . . . . . . . 8
74 nn0re 10534 . . . . . . . . . . 11
7574adantl 456 . . . . . . . . . 10
76 simplrl 744 . . . . . . . . . . . 12
7776adantr 455 . . . . . . . . . . 11
7877nn0red 10582 . . . . . . . . . 10
79 simprl 740 . . . . . . . . . . . . . 14
80 simprr 741 . . . . . . . . . . . . . 14
8176adantr 455 . . . . . . . . . . . . . . 15
82 fznn0 11465 . . . . . . . . . . . . . . 15
8381, 82syl 16 . . . . . . . . . . . . . 14
8479, 80, 83mpbir2and 898 . . . . . . . . . . . . 13
85 simplrr 745 . . . . . . . . . . . . 13
86 fveq2 5661 . . . . . . . . . . . . . . 15
87 fveq2 5661 . . . . . . . . . . . . . . . . . 18
8887fveq2d 5665 . . . . . . . . . . . . . . . . 17
8988fveq2d 5665 . . . . . . . . . . . . . . . 16
90 id 21 . . . . . . . . . . . . . . . 16
9189, 90fveq12d 5667 . . . . . . . . . . . . . . 15
9286, 91sseq12d 3362 . . . . . . . . . . . . . 14
9392rspcva 3049 . . . . . . . . . . . . 13
9484, 85, 93syl2anc 646 . . . . . . . . . . . 12
9568adantr 455 . . . . . . . . . . . . 13
96 fvssunirn 5683 . . . . . . . . . . . . . . . 16
9796, 52syl5ss 3344 . . . . . . . . . . . . . . 15
9827, 49, 10rspcl 17113 . . . . . . . . . . . . . . 15
9969, 97, 98syl2anc 646 . . . . . . . . . . . . . 14
10099adantr 455 . . . . . . . . . . . . 13
10171adantr 455 . . . . . . . . . . . . 13
10268, 3syl 16 . . . . . . . . . . . . . . 15 <