Theorem dgrval

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

	Ref	Expression
Hypothesis	dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion	dgrval	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
3	2	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
4		fveq2	⊢ ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝐹 ) )
5	4 1	eqtr4di	⊢ ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = 𝐴 )
6	5	cnveqd	⊢ ( 𝑓 = 𝐹 → ◡ ( coeff ‘ 𝑓 ) = ◡ 𝐴 )
7	6	imaeq1d	⊢ ( 𝑓 = 𝐹 → ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) = ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) )
8	7	supeq1d	⊢ ( 𝑓 = 𝐹 → sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
9		df-dgr	⊢ deg = ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
10		nn0ssre	⊢ ℕ0 ⊆ ℝ
11		ltso	⊢ < Or ℝ
12		soss	⊢ ( ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0 ) )
13	10 11 12	mp2	⊢ < Or ℕ0
14	13	supex	⊢ sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) ∈ V
15	8 9 14	fvmpt	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
16	3 15	syl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )