Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015) Remove hypothesis. (Revised by SN, 20-May-2025)

	Ref	Expression
Hypotheses	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1bas.u	$$⊢U={\mathrm{Base}}_P$$
Assertion	ply1bas	$$⊢U={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1bas.u	$$⊢U={\mathrm{Base}}_P$$
3		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
5		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
6		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
8	6 7 4	psr1bas2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
9	3 4 5 8	mplbasss	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
10	1 6	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
11	10 7	ressbas2	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_P$$
12	9 11	ax-mp	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_P$$
13	2 12	eqtr4i	$$⊢U={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$