Theorem deg1fval

Description: Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypothesis	deg1fval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
Assertion	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		deg1fval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		oveq2	⊢ ( 𝑟 = 𝑅 → ( 1o mDeg 𝑟 ) = ( 1o mDeg 𝑅 ) )
3		df-deg1	⊢ deg1 = ( 𝑟 ∈ V ↦ ( 1o mDeg 𝑟 ) )
4		ovex	⊢ ( 1o mDeg 𝑅 ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝑅 ∈ V → ( deg1 ‘ 𝑅 ) = ( 1o mDeg 𝑅 ) )
6		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( deg1 ‘ 𝑅 ) = ∅ )
7		reldmmdeg	⊢ Rel dom mDeg
8	7	ovprc2	⊢ ( ¬ 𝑅 ∈ V → ( 1o mDeg 𝑅 ) = ∅ )
9	6 8	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( deg1 ‘ 𝑅 ) = ( 1o mDeg 𝑅 ) )
10	5 9	pm2.61i	⊢ ( deg1 ‘ 𝑅 ) = ( 1o mDeg 𝑅 )
11	1 10	eqtri	⊢ 𝐷 = ( 1o mDeg 𝑅 )