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

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