Metamath Proof Explorer


Theorem 0dgrb

Description: A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion 0dgrb FPolySdegF=0F=×F0

Proof

Step Hyp Ref Expression
1 eqid coeffF=coeffF
2 eqid degF=degF
3 1 2 coeid FPolySF=zk=0degFcoeffFkzk
4 3 adantr FPolySdegF=0F=zk=0degFcoeffFkzk
5 simplr FPolySdegF=0zdegF=0
6 5 oveq2d FPolySdegF=0z0degF=00
7 6 sumeq1d FPolySdegF=0zk=0degFcoeffFkzk=k=00coeffFkzk
8 0z 0
9 exp0 zz0=1
10 9 adantl FPolySdegF=0zz0=1
11 10 oveq2d FPolySdegF=0zcoeffF0z0=coeffF01
12 1 coef3 FPolyScoeffF:0
13 0nn0 00
14 ffvelrn coeffF:000coeffF0
15 12 13 14 sylancl FPolyScoeffF0
16 15 ad2antrr FPolySdegF=0zcoeffF0
17 16 mulid1d FPolySdegF=0zcoeffF01=coeffF0
18 11 17 eqtrd FPolySdegF=0zcoeffF0z0=coeffF0
19 18 16 eqeltrd FPolySdegF=0zcoeffF0z0
20 fveq2 k=0coeffFk=coeffF0
21 oveq2 k=0zk=z0
22 20 21 oveq12d k=0coeffFkzk=coeffF0z0
23 22 fsum1 0coeffF0z0k=00coeffFkzk=coeffF0z0
24 8 19 23 sylancr FPolySdegF=0zk=00coeffFkzk=coeffF0z0
25 24 18 eqtrd FPolySdegF=0zk=00coeffFkzk=coeffF0
26 7 25 eqtrd FPolySdegF=0zk=0degFcoeffFkzk=coeffF0
27 26 mpteq2dva FPolySdegF=0zk=0degFcoeffFkzk=zcoeffF0
28 4 27 eqtrd FPolySdegF=0F=zcoeffF0
29 fconstmpt ×coeffF0=zcoeffF0
30 28 29 eqtr4di FPolySdegF=0F=×coeffF0
31 30 fveq1d FPolySdegF=0F0=×coeffF00
32 0cn 0
33 fvex coeffF0V
34 33 fvconst2 0×coeffF00=coeffF0
35 32 34 ax-mp ×coeffF00=coeffF0
36 31 35 eqtrdi FPolySdegF=0F0=coeffF0
37 36 sneqd FPolySdegF=0F0=coeffF0
38 37 xpeq2d FPolySdegF=0×F0=×coeffF0
39 30 38 eqtr4d FPolySdegF=0F=×F0
40 39 ex FPolySdegF=0F=×F0
41 plyf FPolySF:
42 ffvelrn F:0F0
43 41 32 42 sylancl FPolySF0
44 0dgr F0deg×F0=0
45 43 44 syl FPolySdeg×F0=0
46 fveqeq2 F=×F0degF=0deg×F0=0
47 45 46 syl5ibrcom FPolySF=×F0degF=0
48 40 47 impbid FPolySdegF=0F=×F0