Theorem ressply1bas2

Description: The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	ressply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
	ressply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressply1.b	$$⊢B={\mathrm{Base}}_U$$
	ressply1.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressply1bas2.w	$$⊢W={\mathrm{PwSer}}_1\left(H\right)$$
	ressply1bas2.c	$$⊢C={\mathrm{Base}}_W$$
	ressply1bas2.k	$$⊢K={\mathrm{Base}}_S$$
Assertion	ressply1bas2	$$⊢\phi \to B=C\cap K$$

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		ressply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressply1.b	$$⊢B={\mathrm{Base}}_U$$
5		ressply1.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		ressply1bas2.w	$$⊢W={\mathrm{PwSer}}_1\left(H\right)$$
7		ressply1bas2.c	$$⊢C={\mathrm{Base}}_W$$
8		ressply1bas2.k	$$⊢K={\mathrm{Base}}_S$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
10		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
11	3 6 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
12		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
13	12	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
14		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}H=1_{𝑜}\mathrm{mPwSer}H$$
15	6 7 14	psr1bas2	$$⊢C={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}H\right)}$$
16		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
17	1 16 8	ply1bas	$$⊢K={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	9 2 10 11 13 5 14 15 17	ressmplbas2	$$⊢\phi \to B=C\cap K$$