Metamath Proof Explorer


Theorem mdegldg

Description: A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdegval.d D = I mDeg R
mdegval.p P = I mPoly R
mdegval.b B = Base P
mdegval.z 0 ˙ = 0 R
mdegval.a A = m 0 I | m -1 Fin
mdegval.h H = h A fld h
mdegldg.y Y = 0 P
Assertion mdegldg R Ring F B F Y x A F x 0 ˙ H x = D F

Proof

Step Hyp Ref Expression
1 mdegval.d D = I mDeg R
2 mdegval.p P = I mPoly R
3 mdegval.b B = Base P
4 mdegval.z 0 ˙ = 0 R
5 mdegval.a A = m 0 I | m -1 Fin
6 mdegval.h H = h A fld h
7 mdegldg.y Y = 0 P
8 1 2 3 4 5 6 mdegval F B D F = sup H F supp 0 ˙ * <
9 8 3ad2ant2 R Ring F B F Y D F = sup H F supp 0 ˙ * <
10 5 6 tdeglem1 H : A 0
11 10 a1i R Ring F B F Y H : A 0
12 11 ffund R Ring F B F Y Fun H
13 simp2 R Ring F B F Y F B
14 2 3 4 13 mplelsfi R Ring F B F Y finSupp 0 ˙ F
15 14 fsuppimpd R Ring F B F Y F supp 0 ˙ Fin
16 imafi Fun H F supp 0 ˙ Fin H F supp 0 ˙ Fin
17 12 15 16 syl2anc R Ring F B F Y H F supp 0 ˙ Fin
18 simp3 R Ring F B F Y F Y
19 2 3 mplrcl F B I V
20 19 3ad2ant2 R Ring F B F Y I V
21 ringgrp R Ring R Grp
22 21 3ad2ant1 R Ring F B F Y R Grp
23 2 5 4 7 20 22 mpl0 R Ring F B F Y Y = A × 0 ˙
24 18 23 neeqtrd R Ring F B F Y F A × 0 ˙
25 eqid Base R = Base R
26 2 25 3 5 13 mplelf R Ring F B F Y F : A Base R
27 26 ffnd R Ring F B F Y F Fn A
28 4 fvexi 0 ˙ V
29 ovex 0 I V
30 5 29 rabex2 A V
31 fnsuppeq0 F Fn A A V 0 ˙ V F supp 0 ˙ = F = A × 0 ˙
32 30 31 mp3an2 F Fn A 0 ˙ V F supp 0 ˙ = F = A × 0 ˙
33 27 28 32 sylancl R Ring F B F Y F supp 0 ˙ = F = A × 0 ˙
34 33 necon3bid R Ring F B F Y F supp 0 ˙ F A × 0 ˙
35 24 34 mpbird R Ring F B F Y F supp 0 ˙
36 11 ffnd R Ring F B F Y H Fn A
37 suppssdm F supp 0 ˙ dom F
38 37 26 fssdm R Ring F B F Y F supp 0 ˙ A
39 fnimaeq0 H Fn A F supp 0 ˙ A H F supp 0 ˙ = F supp 0 ˙ =
40 36 38 39 syl2anc R Ring F B F Y H F supp 0 ˙ = F supp 0 ˙ =
41 40 necon3bid R Ring F B F Y H F supp 0 ˙ F supp 0 ˙
42 35 41 mpbird R Ring F B F Y H F supp 0 ˙
43 imassrn H F supp 0 ˙ ran H
44 11 frnd R Ring F B F Y ran H 0
45 43 44 sstrid R Ring F B F Y H F supp 0 ˙ 0
46 nn0ssre 0
47 ressxr *
48 46 47 sstri 0 *
49 45 48 sstrdi R Ring F B F Y H F supp 0 ˙ *
50 xrltso < Or *
51 fisupcl < Or * H F supp 0 ˙ Fin H F supp 0 ˙ H F supp 0 ˙ * sup H F supp 0 ˙ * < H F supp 0 ˙
52 50 51 mpan H F supp 0 ˙ Fin H F supp 0 ˙ H F supp 0 ˙ * sup H F supp 0 ˙ * < H F supp 0 ˙
53 17 42 49 52 syl3anc R Ring F B F Y sup H F supp 0 ˙ * < H F supp 0 ˙
54 9 53 eqeltrd R Ring F B F Y D F H F supp 0 ˙
55 36 38 fvelimabd R Ring F B F Y D F H F supp 0 ˙ x supp 0 ˙ F H x = D F
56 rexsupp F Fn A A V 0 ˙ V x supp 0 ˙ F H x = D F x A F x 0 ˙ H x = D F
57 30 28 56 mp3an23 F Fn A x supp 0 ˙ F H x = D F x A F x 0 ˙ H x = D F
58 27 57 syl R Ring F B F Y x supp 0 ˙ F H x = D F x A F x 0 ˙ H x = D F
59 55 58 bitrd R Ring F B F Y D F H F supp 0 ˙ x A F x 0 ˙ H x = D F
60 54 59 mpbid R Ring F B F Y x A F x 0 ˙ H x = D F