Theorem ply1basfvi

Description: Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Assertion	ply1basfvi	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_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	eqcomd	$$⊢R\in \mathrm{V}\to R=\mathrm{I}\left(R\right)$$
3	2	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)$$
4	3	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}$$
5		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
6		00ply1bas	$$⊢\varnothing ={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
7	5 6	eqtr3i	$$⊢{\mathrm{Base}}_{\varnothing }={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
8		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
9	8	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{\varnothing }$$
10		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\varnothing$$
11	10	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{Poly}}_1\left(\varnothing \right)$$
12	11	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
13	7 9 12	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}$$
14	4 13	pm2.61i	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}$$