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
|- ( F e. ( Poly ` S ) -> ( ( deg ` F ) = 0 <-> F = ( CC X. { ( F ` 0 ) } ) ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( coeff ` F ) = ( coeff ` F )
2 eqid
 |-  ( deg ` F ) = ( deg ` F )
3 1 2 coeid
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) )
4 3 adantr
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) )
5 simplr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( deg ` F ) = 0 )
6 5 oveq2d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( 0 ... ( deg ` F ) ) = ( 0 ... 0 ) )
7 6 sumeq1d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) )
8 0z
 |-  0 e. ZZ
9 exp0
 |-  ( z e. CC -> ( z ^ 0 ) = 1 )
10 9 adantl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( z ^ 0 ) = 1 )
11 10 oveq2d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) = ( ( ( coeff ` F ) ` 0 ) x. 1 ) )
12 1 coef3
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
13 0nn0
 |-  0 e. NN0
14 ffvelrn
 |-  ( ( ( coeff ` F ) : NN0 --> CC /\ 0 e. NN0 ) -> ( ( coeff ` F ) ` 0 ) e. CC )
15 12 13 14 sylancl
 |-  ( F e. ( Poly ` S ) -> ( ( coeff ` F ) ` 0 ) e. CC )
16 15 ad2antrr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( ( coeff ` F ) ` 0 ) e. CC )
17 16 mulid1d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( ( ( coeff ` F ) ` 0 ) x. 1 ) = ( ( coeff ` F ) ` 0 ) )
18 11 17 eqtrd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) = ( ( coeff ` F ) ` 0 ) )
19 18 16 eqeltrd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) e. CC )
20 fveq2
 |-  ( k = 0 -> ( ( coeff ` F ) ` k ) = ( ( coeff ` F ) ` 0 ) )
21 oveq2
 |-  ( k = 0 -> ( z ^ k ) = ( z ^ 0 ) )
22 20 21 oveq12d
 |-  ( k = 0 -> ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) )
23 22 fsum1
 |-  ( ( 0 e. ZZ /\ ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) )
24 8 19 23 sylancr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` F ) ` 0 ) x. ( z ^ 0 ) ) )
25 24 18 eqtrd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = ( ( coeff ` F ) ` 0 ) )
26 7 25 eqtrd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) /\ z e. CC ) -> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) = ( ( coeff ` F ) ` 0 ) )
27 26 mpteq2dva
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> ( ( coeff ` F ) ` 0 ) ) )
28 4 27 eqtrd
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> F = ( z e. CC |-> ( ( coeff ` F ) ` 0 ) ) )
29 fconstmpt
 |-  ( CC X. { ( ( coeff ` F ) ` 0 ) } ) = ( z e. CC |-> ( ( coeff ` F ) ` 0 ) )
30 28 29 eqtr4di
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> F = ( CC X. { ( ( coeff ` F ) ` 0 ) } ) )
31 30 fveq1d
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> ( F ` 0 ) = ( ( CC X. { ( ( coeff ` F ) ` 0 ) } ) ` 0 ) )
32 0cn
 |-  0 e. CC
33 fvex
 |-  ( ( coeff ` F ) ` 0 ) e. _V
34 33 fvconst2
 |-  ( 0 e. CC -> ( ( CC X. { ( ( coeff ` F ) ` 0 ) } ) ` 0 ) = ( ( coeff ` F ) ` 0 ) )
35 32 34 ax-mp
 |-  ( ( CC X. { ( ( coeff ` F ) ` 0 ) } ) ` 0 ) = ( ( coeff ` F ) ` 0 )
36 31 35 eqtrdi
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> ( F ` 0 ) = ( ( coeff ` F ) ` 0 ) )
37 36 sneqd
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> { ( F ` 0 ) } = { ( ( coeff ` F ) ` 0 ) } )
38 37 xpeq2d
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> ( CC X. { ( F ` 0 ) } ) = ( CC X. { ( ( coeff ` F ) ` 0 ) } ) )
39 30 38 eqtr4d
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) = 0 ) -> F = ( CC X. { ( F ` 0 ) } ) )
40 39 ex
 |-  ( F e. ( Poly ` S ) -> ( ( deg ` F ) = 0 -> F = ( CC X. { ( F ` 0 ) } ) ) )
41 plyf
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
42 ffvelrn
 |-  ( ( F : CC --> CC /\ 0 e. CC ) -> ( F ` 0 ) e. CC )
43 41 32 42 sylancl
 |-  ( F e. ( Poly ` S ) -> ( F ` 0 ) e. CC )
44 0dgr
 |-  ( ( F ` 0 ) e. CC -> ( deg ` ( CC X. { ( F ` 0 ) } ) ) = 0 )
45 43 44 syl
 |-  ( F e. ( Poly ` S ) -> ( deg ` ( CC X. { ( F ` 0 ) } ) ) = 0 )
46 fveqeq2
 |-  ( F = ( CC X. { ( F ` 0 ) } ) -> ( ( deg ` F ) = 0 <-> ( deg ` ( CC X. { ( F ` 0 ) } ) ) = 0 ) )
47 45 46 syl5ibrcom
 |-  ( F e. ( Poly ` S ) -> ( F = ( CC X. { ( F ` 0 ) } ) -> ( deg ` F ) = 0 ) )
48 40 47 impbid
 |-  ( F e. ( Poly ` S ) -> ( ( deg ` F ) = 0 <-> F = ( CC X. { ( F ` 0 ) } ) ) )