Metamath Proof Explorer


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