Metamath Proof Explorer


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