Theorem deg1cl

Description: Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	deg1cl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4	1	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
7	2 6 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	4 5 7	mdegcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )