Theorem deg1fvi

Description: Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	deg1fvi	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
2	1	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{deg}}_1\left(R\right)$$
3		eqid	$$⊢{\mathrm{deg}}_1\left(\varnothing \right)={\mathrm{deg}}_1\left(\varnothing \right)$$
4		eqid	$$⊢{\mathrm{Poly}}_1\left(\varnothing \right)={\mathrm{Poly}}_1\left(\varnothing \right)$$
5		00ply1bas	$$⊢\varnothing ={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
6	3 4 5	deg1xrf	$$⊢{\mathrm{deg}}_1\left(\varnothing \right):\varnothing ⟶{ℝ}^{*}$$
7		ffn	$$⊢{\mathrm{deg}}_1\left(\varnothing \right):\varnothing ⟶{ℝ}^{*}\to {\mathrm{deg}}_1\left(\varnothing \right)Fn\varnothing$$
8	6 7	ax-mp	$$⊢{\mathrm{deg}}_1\left(\varnothing \right)Fn\varnothing$$
9		fn0	$$⊢{\mathrm{deg}}_1\left(\varnothing \right)Fn\varnothing \leftrightarrow {\mathrm{deg}}_1\left(\varnothing \right)=\varnothing$$
10	8 9	mpbi	$$⊢{\mathrm{deg}}_1\left(\varnothing \right)=\varnothing$$
11		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\varnothing$$
12	11	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{deg}}_1\left(\varnothing \right)$$
13		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{deg}}_1\left(R\right)=\varnothing$$
14	10 12 13	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{deg}}_1\left(R\right)$$
15	2 14	pm2.61i	$$⊢{\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{deg}}_1\left(R\right)$$
16	15	eqcomi	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(\mathrm{I}\left(R\right)\right)$$