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

Metamath Proof Explorer

Theorem deg1xrf

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

Step	Hyp	Ref	Expression
1		deg1xrf.d	$⊢ D = \deg_{1} (R)$
2		deg1xrf.p	$⊢ P = {Poly}_{1} (R)$
3		deg1xrf.b	$⊢ B = {Base}_{P}$
4	1	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
5		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
6	2 3	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
7	4 5 6	mdegxrf	$⊢ D : B ⟶ ℝ^{*}$