Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1val.2	$$⊢S={\mathrm{PwSer}}_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		ply1val.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
3		ply1bas.u	$$⊢U={\mathrm{Base}}_P$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
7		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
8	2 7 5	psr1bas2	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
9	4 5 6 8	mplbasss	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\subseteq {\mathrm{Base}}_S$$
10	1 2	ply1val	$$⊢P=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
11	10 7	ressbas2	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\subseteq {\mathrm{Base}}_S\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	3 12	eqtr4i	$$⊢U={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$