Metamath Proof Explorer


Theorem dgrval

Description: Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypothesis dgrval.1
|- A = ( coeff ` F )
Assertion dgrval
|- ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )

Proof

Step Hyp Ref Expression
1 dgrval.1
 |-  A = ( coeff ` F )
2 plyssc
 |-  ( Poly ` S ) C_ ( Poly ` CC )
3 2 sseli
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
4 fveq2
 |-  ( f = F -> ( coeff ` f ) = ( coeff ` F ) )
5 4 1 eqtr4di
 |-  ( f = F -> ( coeff ` f ) = A )
6 5 cnveqd
 |-  ( f = F -> `' ( coeff ` f ) = `' A )
7 6 imaeq1d
 |-  ( f = F -> ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) = ( `' A " ( CC \ { 0 } ) ) )
8 7 supeq1d
 |-  ( f = F -> sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
9 df-dgr
 |-  deg = ( f e. ( Poly ` CC ) |-> sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )
10 nn0ssre
 |-  NN0 C_ RR
11 ltso
 |-  < Or RR
12 soss
 |-  ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
13 10 11 12 mp2
 |-  < Or NN0
14 13 supex
 |-  sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) e. _V
15 8 9 14 fvmpt
 |-  ( F e. ( Poly ` CC ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
16 3 15 syl
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )