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 ⊢ 𝐴 = ( 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 , < ) )