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

Theorem hbt 29946
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 29928 . . 3
2 hbt.p . . . 4
32ply1rng 17883 . . 3
41, 3syl 16 . 2
5 eqid 2454 . . . . . . . 8
6 eqid 2454 . . . . . . . 8
75, 6islnr3 29931 . . . . . . 7
87simprbi 464 . . . . . 6
98adantr 465 . . . . 5
10 eqid 2454 . . . . . . 7
11 eqid 2454 . . . . . . 7
122, 10, 11, 6hbtlem7 29941 . . . . . 6
131, 12sylan 471 . . . . 5
141ad2antrr 725 . . . . . . 7
15 simplr 754 . . . . . . 7
16 simpr 461 . . . . . . 7
17 peano2nn0 10758 . . . . . . . 8
1817adantl 466 . . . . . . 7
19 nn0re 10726 . . . . . . . . 9
2019lep1d 10401 . . . . . . . 8
2120adantl 466 . . . . . . 7
222, 10, 11, 14, 15, 16, 18, 21hbtlem4 29942 . . . . . 6
2322ralrimiva 2831 . . . . 5
24 nacsfix 29508 . . . . 5
259, 13, 23, 24syl3anc 1219 . . . 4
26 fzfi 11939 . . . . . . 7
27 eqid 2454 . . . . . . . . 9
28 simpll 753 . . . . . . . . 9
29 simplr 754 . . . . . . . . 9
30 elfznn0 11626 . . . . . . . . . 10
3130adantl 466 . . . . . . . . 9
322, 10, 11, 27, 28, 29, 31hbtlem6 29945 . . . . . . . 8
3332ralrimiva 2831 . . . . . . 7
34 fveq2 5813 . . . . . . . . . . 11
3534fveq2d 5817 . . . . . . . . . 10
3635fveq1d 5815 . . . . . . . . 9
3736sseq2d 3498 . . . . . . . 8
3837ac6sfi 7691 . . . . . . 7
3926, 33, 38sylancr 663 . . . . . 6
4039adantr 465 . . . . 5
41 frn 5685 . . . . . . . . . . . . 13
4241ad2antrl 727 . . . . . . . . . . . 12
43 inss1 3684 . . . . . . . . . . . 12
4442, 43syl6ss 3482 . . . . . . . . . . 11
4544unissd 4232 . . . . . . . . . 10
46 unipw 4659 . . . . . . . . . 10
4745, 46syl6sseq 3516 . . . . . . . . 9
48 simpllr 758 . . . . . . . . . 10
49 eqid 2454 . . . . . . . . . . 11
5049, 10lidlss 17467 . . . . . . . . . 10
5148, 50syl 16 . . . . . . . . 9
5247, 51sstrd 3480 . . . . . . . 8
53 fvex 5823 . . . . . . . . 9
5453elpw2 4573 . . . . . . . 8
5552, 54sylibr 212 . . . . . . 7
56 simprl 755 . . . . . . . . 9
57 ffn 5679 . . . . . . . . 9
58 fniunfv 6089 . . . . . . . . 9
5956, 57, 583syl 20 . . . . . . . 8
60 inss2 3685 . . . . . . . . . . 11
6156ffvelrnda 5966 . . . . . . . . . . 11
6260, 61sseldi 3468 . . . . . . . . . 10
6362ralrimiva 2831 . . . . . . . . 9
64 iunfi 7734 . . . . . . . . 9
6526, 63, 64sylancr 663 . . . . . . . 8
6659, 65eqeltrrd 2543 . . . . . . 7
6755, 66elind 3654 . . . . . 6
681ad3antrrr 729 . . . . . . . 8
694ad3antrrr 729 . . . . . . . . 9
7027, 49, 10rspcl 17480 . . . . . . . . 9
7169, 52, 70syl2anc 661 . . . . . . . 8
7227, 10rspssp 17484 . . . . . . . . 9
7369, 48, 47, 72syl3anc 1219 . . . . . . . 8
74 nn0re 10726 . . . . . . . . . . 11
7574adantl 466 . . . . . . . . . 10
76 simplrl 759 . . . . . . . . . . . 12
7776adantr 465 . . . . . . . . . . 11
7877nn0red 10775 . . . . . . . . . 10
79 simprl 755 . . . . . . . . . . . . . 14
80 simprr 756 . . . . . . . . . . . . . 14
8176adantr 465 . . . . . . . . . . . . . . 15
82 fznn0 11669 . . . . . . . . . . . . . . 15
8381, 82syl 16 . . . . . . . . . . . . . 14
8479, 80, 83mpbir2and 913 . . . . . . . . . . . . 13
85 simplrr 760 . . . . . . . . . . . . 13
86 fveq2 5813 . . . . . . . . . . . . . . 15
87 fveq2 5813 . . . . . . . . . . . . . . . . . 18
8887fveq2d 5817 . . . . . . . . . . . . . . . . 17
8988fveq2d 5817 . . . . . . . . . . . . . . . 16
90 id 22 . . . . . . . . . . . . . . . 16
9189, 90fveq12d 5819 . . . . . . . . . . . . . . 15
9286, 91sseq12d 3499 . . . . . . . . . . . . . 14
9392rspcva 3180 . . . . . . . . . . . . 13
9484, 85, 93syl2anc 661 . . . . . . . . . . . 12
9568adantr 465 . . . . . . . . . . . . 13
96 fvssunirn 5836 . . . . . . . . . . . . . . . 16
9796, 52syl5ss 3481 . . . . . . . . . . . . . . 15
9827, 49, 10rspcl 17480 . . . . . . . . . . . . . . 15
9969, 97, 98syl2anc 661 . . . . . . . . . . . . . 14
10099adantr 465 . . . . . . . . . . . . 13
10171adantr 465 . . . . . . . . . . . . 13
10268, 3syl 16 . . . . . . . . . . . . . . 15