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