Theorem ressply1bas

Description: A restricted polynomial algebra has the same base set. (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)$$
	ressply1.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
Assertion	ressply1bas	$$⊢\phi \to B={\mathrm{Base}}_P$$

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		ressply1.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
7		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
8		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10	1 2 3 4 5 7 8 9	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S$$
11		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S\subseteq {\mathrm{Base}}_S$$
12	10 11	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_S$$
13	6 9	ressbas2	$$⊢B\subseteq {\mathrm{Base}}_S\to B={\mathrm{Base}}_P$$
14	12 13	syl	$$⊢\phi \to B={\mathrm{Base}}_P$$