Theorem ply1basOLD

Description: Obsolete version of ply1bas as of 20-May-2025. (Contributed by Mario Carneiro, 9-Feb-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1lss.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
	ply1lss.u	$$⊢U={\mathrm{Base}}_P$$
Assertion	ply1basOLD	$$⊢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		ply1lss.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
3		ply1lss.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)}$$