Theorem deg1xrcl

Description: Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	deg1xrcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4	1 2 3	deg1xrf	⊢ 𝐷 : 𝐵 ⟶ ℝ*
5	4	ffvelcdmi	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )