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 ⊢ A = coeff ⁡ F
Assertion dgrval ⊢ F ∈ Poly ⁡ S → deg ⁡ F = sup A -1 ℂ ∖ 0 ℕ 0 <

Proof

Step Hyp Ref Expression
1 dgrval.1 ⊢ A = coeff ⁡ F
2 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
3 2 sseli ⊢ F ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
4 fveq2 ⊢ f = F → coeff ⁡ f = coeff ⁡ F
5 4 1 eqtr4di ⊢ f = F → coeff ⁡ f = A
6 5 cnveqd ⊢ f = F → coeff ⁡ f -1 = A -1
7 6 imaeq1d ⊢ f = F → coeff ⁡ f -1 ℂ ∖ 0 = A -1 ℂ ∖ 0
8 7 supeq1d ⊢ f = F → sup coeff ⁡ f -1 ℂ ∖ 0 ℕ 0 < = sup A -1 ℂ ∖ 0 ℕ 0 <
9 df-dgr ⊢ deg = f ∈ Poly ⁡ ℂ ⟼ sup coeff ⁡ f -1 ℂ ∖ 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 A -1 ℂ ∖ 0 ℕ 0 < ∈ V
15 8 9 14 fvmpt ⊢ F ∈ Poly ⁡ ℂ → deg ⁡ F = sup A -1 ℂ ∖ 0 ℕ 0 <
16 3 15 syl ⊢ F ∈ Poly ⁡ S → deg ⁡ F = sup A -1 ℂ ∖ 0 ℕ 0 <