This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ D = \deg_{1} (R)$
	Assertion	deg1fval	$⊢ D = 1_{𝑜} mDeg R$

Proof

Step	Hyp	Ref	Expression
1		deg1fval.d	$⊢ D = \deg_{1} (R)$
2		oveq2	$⊢ r = R \to 1_{𝑜} mDeg r = 1_{𝑜} mDeg R$
3		df-deg1	$⊢ \deg_{1} = (r \in V ⟼ 1_{𝑜} mDeg r)$
4		ovex	$⊢ 1_{𝑜} mDeg R \in V$
5	2 3 4	fvmpt	$⊢ R \in V \to \deg_{1} (R) = 1_{𝑜} mDeg R$
6		fvprc	$⊢ \neg R \in V \to \deg_{1} (R) = \emptyset$
7		reldmmdeg	$⊢ Rel dom mDeg$
8	7	ovprc2	$⊢ \neg R \in V \to 1_{𝑜} mDeg R = \emptyset$
9	6 8	eqtr4d	$⊢ \neg R \in V \to \deg_{1} (R) = 1_{𝑜} mDeg R$
10	5 9	pm2.61i	$⊢ \deg_{1} (R) = 1_{𝑜} mDeg R$
11	1 10	eqtri	$⊢ D = 1_{𝑜} mDeg R$