Metamath Proof Explorer


Theorem mdegle0

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y Y = I mPoly R
mdegaddle.d D = I mDeg R
mdegaddle.i φ I V
mdegaddle.r φ R Ring
mdegle0.b B = Base Y
mdegle0.a A = algSc Y
mdegle0.f φ F B
Assertion mdegle0 φ D F 0 F = A F I × 0

Proof

Step Hyp Ref Expression
1 mdegaddle.y Y = I mPoly R
2 mdegaddle.d D = I mDeg R
3 mdegaddle.i φ I V
4 mdegaddle.r φ R Ring
5 mdegle0.b B = Base Y
6 mdegle0.a A = algSc Y
7 mdegle0.f φ F B
8 0xr 0 *
9 eqid 0 R = 0 R
10 eqid a 0 I | a -1 Fin = a 0 I | a -1 Fin
11 eqid b a 0 I | a -1 Fin fld b = b a 0 I | a -1 Fin fld b
12 2 1 5 9 10 11 mdegleb F B 0 * D F 0 x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R
13 7 8 12 sylancl φ D F 0 x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R
14 10 11 tdeglem1 b a 0 I | a -1 Fin fld b : a 0 I | a -1 Fin 0
15 14 a1i φ b a 0 I | a -1 Fin fld b : a 0 I | a -1 Fin 0
16 15 ffvelrnda φ x a 0 I | a -1 Fin b a 0 I | a -1 Fin fld b x 0
17 nn0re b a 0 I | a -1 Fin fld b x 0 b a 0 I | a -1 Fin fld b x
18 nn0ge0 b a 0 I | a -1 Fin fld b x 0 0 b a 0 I | a -1 Fin fld b x
19 17 18 jca b a 0 I | a -1 Fin fld b x 0 b a 0 I | a -1 Fin fld b x 0 b a 0 I | a -1 Fin fld b x
20 ne0gt0 b a 0 I | a -1 Fin fld b x 0 b a 0 I | a -1 Fin fld b x b a 0 I | a -1 Fin fld b x 0 0 < b a 0 I | a -1 Fin fld b x
21 16 19 20 3syl φ x a 0 I | a -1 Fin b a 0 I | a -1 Fin fld b x 0 0 < b a 0 I | a -1 Fin fld b x
22 10 11 tdeglem4 x a 0 I | a -1 Fin b a 0 I | a -1 Fin fld b x = 0 x = I × 0
23 22 adantl φ x a 0 I | a -1 Fin b a 0 I | a -1 Fin fld b x = 0 x = I × 0
24 23 necon3abid φ x a 0 I | a -1 Fin b a 0 I | a -1 Fin fld b x 0 ¬ x = I × 0
25 21 24 bitr3d φ x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x ¬ x = I × 0
26 25 imbi1d φ x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R ¬ x = I × 0 F x = 0 R
27 eqeq2 F I × 0 = if x = I × 0 F I × 0 0 R F x = F I × 0 F x = if x = I × 0 F I × 0 0 R
28 27 bibi1d F I × 0 = if x = I × 0 F I × 0 0 R F x = F I × 0 ¬ x = I × 0 F x = 0 R F x = if x = I × 0 F I × 0 0 R ¬ x = I × 0 F x = 0 R
29 eqeq2 0 R = if x = I × 0 F I × 0 0 R F x = 0 R F x = if x = I × 0 F I × 0 0 R
30 29 bibi1d 0 R = if x = I × 0 F I × 0 0 R F x = 0 R ¬ x = I × 0 F x = 0 R F x = if x = I × 0 F I × 0 0 R ¬ x = I × 0 F x = 0 R
31 fveq2 x = I × 0 F x = F I × 0
32 pm2.24 x = I × 0 ¬ x = I × 0 F x = 0 R
33 31 32 2thd x = I × 0 F x = F I × 0 ¬ x = I × 0 F x = 0 R
34 33 adantl φ x = I × 0 F x = F I × 0 ¬ x = I × 0 F x = 0 R
35 biimt ¬ x = I × 0 F x = 0 R ¬ x = I × 0 F x = 0 R
36 35 adantl φ ¬ x = I × 0 F x = 0 R ¬ x = I × 0 F x = 0 R
37 28 30 34 36 ifbothda φ F x = if x = I × 0 F I × 0 0 R ¬ x = I × 0 F x = 0 R
38 37 adantr φ x a 0 I | a -1 Fin F x = if x = I × 0 F I × 0 0 R ¬ x = I × 0 F x = 0 R
39 26 38 bitr4d φ x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R F x = if x = I × 0 F I × 0 0 R
40 39 ralbidva φ x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R x a 0 I | a -1 Fin F x = if x = I × 0 F I × 0 0 R
41 eqid Base R = Base R
42 1 41 5 10 7 mplelf φ F : a 0 I | a -1 Fin Base R
43 42 feqmptd φ F = x a 0 I | a -1 Fin F x
44 10 psrbag0 I V I × 0 a 0 I | a -1 Fin
45 3 44 syl φ I × 0 a 0 I | a -1 Fin
46 42 45 ffvelrnd φ F I × 0 Base R
47 1 10 9 41 6 3 4 46 mplascl φ A F I × 0 = x a 0 I | a -1 Fin if x = I × 0 F I × 0 0 R
48 43 47 eqeq12d φ F = A F I × 0 x a 0 I | a -1 Fin F x = x a 0 I | a -1 Fin if x = I × 0 F I × 0 0 R
49 fvex F x V
50 49 rgenw x a 0 I | a -1 Fin F x V
51 mpteqb x a 0 I | a -1 Fin F x V x a 0 I | a -1 Fin F x = x a 0 I | a -1 Fin if x = I × 0 F I × 0 0 R x a 0 I | a -1 Fin F x = if x = I × 0 F I × 0 0 R
52 50 51 mp1i φ x a 0 I | a -1 Fin F x = x a 0 I | a -1 Fin if x = I × 0 F I × 0 0 R x a 0 I | a -1 Fin F x = if x = I × 0 F I × 0 0 R
53 48 52 bitrd φ F = A F I × 0 x a 0 I | a -1 Fin F x = if x = I × 0 F I × 0 0 R
54 40 53 bitr4d φ x a 0 I | a -1 Fin 0 < b a 0 I | a -1 Fin fld b x F x = 0 R F = A F I × 0
55 13 54 bitrd φ D F 0 F = A F I × 0