Theorem ressmplbas

Description: A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	ressmpl.s	$$⊢S=I\mathrm{mPoly}R$$
	ressmpl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressmpl.u	$$⊢U=I\mathrm{mPoly}H$$
	ressmpl.b	$$⊢B={\mathrm{Base}}_U$$
	ressmpl.1	$$⊢\phi \to I\in V$$
	ressmpl.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressmpl.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
Assertion	ressmplbas	$$⊢\phi \to B={\mathrm{Base}}_P$$

Proof

Step	Hyp	Ref	Expression
1		ressmpl.s	$$⊢S=I\mathrm{mPoly}R$$
2		ressmpl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressmpl.u	$$⊢U=I\mathrm{mPoly}H$$
4		ressmpl.b	$$⊢B={\mathrm{Base}}_U$$
5		ressmpl.1	$$⊢\phi \to I\in V$$
6		ressmpl.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
7		ressmpl.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
8		eqid	$$⊢I\mathrm{mPwSer}H=I\mathrm{mPwSer}H$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
10		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
11	1 2 3 4 5 6 8 9 10	ressmplbas2	$$⊢\phi \to B={\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\cap {\mathrm{Base}}_S$$
12		inss2	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\cap {\mathrm{Base}}_S\subseteq {\mathrm{Base}}_S$$
13	11 12	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_S$$
14	7 10	ressbas2	$$⊢B\subseteq {\mathrm{Base}}_S\to B={\mathrm{Base}}_P$$
15	13 14	syl	$$⊢\phi \to B={\mathrm{Base}}_P$$