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