This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0dgr

Description: A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion 0dgr 
|- ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  CC C_ CC
2 plyconst 
 |-  ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
3 1 2 mpan 
 |-  ( A e. CC -> ( CC X. { A } ) e. ( Poly ` CC ) )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( A e. CC -> 0 e. NN0 )
6 simpl 
 |-  ( ( A e. CC /\ k e. ( 0 ... 0 ) ) -> A e. CC )
7 fconstmpt 
 |-  ( CC X. { A } ) = ( z e. CC |-> A )
8 0z 
 |-  0 e. ZZ
9 exp0 
 |-  ( z e. CC -> ( z ^ 0 ) = 1 )
10 9 oveq2d 
 |-  ( z e. CC -> ( A x. ( z ^ 0 ) ) = ( A x. 1 ) )
11 mulrid 
 |-  ( A e. CC -> ( A x. 1 ) = A )
12 10 11 sylan9eqr 
 |-  ( ( A e. CC /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = A )
13 simpl 
 |-  ( ( A e. CC /\ z e. CC ) -> A e. CC )
14 12 13 eqeltrd 
 |-  ( ( A e. CC /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) e. CC )
15 oveq2 
 |-  ( k = 0 -> ( z ^ k ) = ( z ^ 0 ) )
16 15 oveq2d 
 |-  ( k = 0 -> ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
17 16 fsum1 
 |-  ( ( 0 e. ZZ /\ ( A x. ( z ^ 0 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
18 8 14 17 sylancr 
 |-  ( ( A e. CC /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
19 18 12 eqtrd 
 |-  ( ( A e. CC /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = A )
20 19 mpteq2dva 
 |-  ( A e. CC -> ( z e. CC |-> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) ) = ( z e. CC |-> A ) )
21 7 20 eqtr4id 
 |-  ( A e. CC -> ( CC X. { A } ) = ( z e. CC |-> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) ) )
22 3 5 6 21 dgrle 
 |-  ( A e. CC -> ( deg ` ( CC X. { A } ) ) <_ 0 )
23 dgrcl 
 |-  ( ( CC X. { A } ) e. ( Poly ` CC ) -> ( deg ` ( CC X. { A } ) ) e. NN0 )
24 nn0le0eq0 
 |-  ( ( deg ` ( CC X. { A } ) ) e. NN0 -> ( ( deg ` ( CC X. { A } ) ) <_ 0 <-> ( deg ` ( CC X. { A } ) ) = 0 ) )
25 3 23 24 3syl 
 |-  ( A e. CC -> ( ( deg ` ( CC X. { A } ) ) <_ 0 <-> ( deg ` ( CC X. { A } ) ) = 0 ) )
26 22 25 mpbid 
 |-  ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 )