Metamath Proof Explorer


Theorem mdeg0

Description: Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdeg0.d D = I mDeg R
mdeg0.p P = I mPoly R
mdeg0.z 0 ˙ = 0 P
Assertion mdeg0 I V R Ring D 0 ˙ = −∞

Proof

Step Hyp Ref Expression
1 mdeg0.d D = I mDeg R
2 mdeg0.p P = I mPoly R
3 mdeg0.z 0 ˙ = 0 P
4 ringgrp R Ring R Grp
5 2 mplgrp I V R Grp P Grp
6 4 5 sylan2 I V R Ring P Grp
7 eqid Base P = Base P
8 7 3 grpidcl P Grp 0 ˙ Base P
9 eqid 0 R = 0 R
10 eqid x 0 I | x -1 Fin = x 0 I | x -1 Fin
11 eqid y x 0 I | x -1 Fin fld y = y x 0 I | x -1 Fin fld y
12 1 2 7 9 10 11 mdegval 0 ˙ Base P D 0 ˙ = sup y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R * <
13 6 8 12 3syl I V R Ring D 0 ˙ = sup y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R * <
14 simpl I V R Ring I V
15 4 adantl I V R Ring R Grp
16 2 10 9 3 14 15 mpl0 I V R Ring 0 ˙ = x 0 I | x -1 Fin × 0 R
17 fvex 0 R V
18 fnconstg 0 R V x 0 I | x -1 Fin × 0 R Fn x 0 I | x -1 Fin
19 17 18 mp1i I V R Ring x 0 I | x -1 Fin × 0 R Fn x 0 I | x -1 Fin
20 16 fneq1d I V R Ring 0 ˙ Fn x 0 I | x -1 Fin x 0 I | x -1 Fin × 0 R Fn x 0 I | x -1 Fin
21 19 20 mpbird I V R Ring 0 ˙ Fn x 0 I | x -1 Fin
22 ovex 0 I V
23 22 rabex x 0 I | x -1 Fin V
24 23 a1i I V R Ring x 0 I | x -1 Fin V
25 17 a1i I V R Ring 0 R V
26 fnsuppeq0 0 ˙ Fn x 0 I | x -1 Fin x 0 I | x -1 Fin V 0 R V 0 ˙ supp 0 R = 0 ˙ = x 0 I | x -1 Fin × 0 R
27 21 24 25 26 syl3anc I V R Ring 0 ˙ supp 0 R = 0 ˙ = x 0 I | x -1 Fin × 0 R
28 16 27 mpbird I V R Ring 0 ˙ supp 0 R =
29 28 imaeq2d I V R Ring y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R = y x 0 I | x -1 Fin fld y
30 ima0 y x 0 I | x -1 Fin fld y =
31 29 30 eqtrdi I V R Ring y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R =
32 31 supeq1d I V R Ring sup y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R * < = sup * <
33 xrsup0 sup * < = −∞
34 32 33 eqtrdi I V R Ring sup y x 0 I | x -1 Fin fld y 0 ˙ supp 0 R * < = −∞
35 13 34 eqtrd I V R Ring D 0 ˙ = −∞