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