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 ) } ) ) )