Theorem ressmplbas2

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	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)$$
	ressmplbas2.w	$$⊢W=I\mathrm{mPwSer}H$$
	ressmplbas2.c	$$⊢C={\mathrm{Base}}_W$$
	ressmplbas2.k	$$⊢K={\mathrm{Base}}_S$$
Assertion	ressmplbas2	$$⊢\phi \to B=C\cap K$$

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		ressmplbas2.w	$$⊢W=I\mathrm{mPwSer}H$$
8		ressmplbas2.c	$$⊢C={\mathrm{Base}}_W$$
9		ressmplbas2.k	$$⊢K={\mathrm{Base}}_S$$
10		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
11	10 2 7 8	subrgpsr	$$⊢\left(I\in V\wedge T\in \mathrm{SubRing}\left(R\right)\right)\to C\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
12	5 6 11	syl2anc	$$⊢\phi \to C\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14	13	subrgss	$$⊢C\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)\to C\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
15	12 14	syl	$$⊢\phi \to C\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
16		df-ss	$$⊢C\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\leftrightarrow C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}=C$$
17	15 16	sylib	$$⊢\phi \to C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}=C$$
18		eqid	$$⊢0_R=0_R$$
19	2 18	subrg0	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 0_R=0_H$$
20	6 19	syl	$$⊢\phi \to 0_R=0_H$$
21	20	breq2d	$$⊢\phi \to \left({finSupp}_{0_R}\left(f\right)\leftrightarrow {finSupp}_{0_H}\left(f\right)\right)$$
22	21	abbidv	$$⊢\phi \to \left\{f|{finSupp}_{0_R}\left(f\right)\right\}=\left\{f|{finSupp}_{0_H}\left(f\right)\right\}$$
23	17 22	ineq12d	$$⊢\phi \to \left(C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}=C\cap \left\{f|{finSupp}_{0_H}\left(f\right)\right\}$$
24	23	eqcomd	$$⊢\phi \to C\cap \left\{f|{finSupp}_{0_H}\left(f\right)\right\}=\left(C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}$$
25		eqid	$$⊢0_H=0_H$$
26	3 7 8 25 4	mplbas	$$⊢B=\left\{f\in C|{finSupp}_{0_H}\left(f\right)\right\}$$
27		dfrab3	$$⊢\left\{f\in C|{finSupp}_{0_H}\left(f\right)\right\}=C\cap \left\{f|{finSupp}_{0_H}\left(f\right)\right\}$$
28	26 27	eqtri	$$⊢B=C\cap \left\{f|{finSupp}_{0_H}\left(f\right)\right\}$$
29	1 10 13 18 9	mplbas	$$⊢K=\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}|{finSupp}_{0_R}\left(f\right)\right\}$$
30		dfrab3	$$⊢\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}|{finSupp}_{0_R}\left(f\right)\right\}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}$$
31	29 30	eqtri	$$⊢K={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}$$
32	31	ineq2i	$$⊢C\cap K=C\cap \left({\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}\right)$$
33		inass	$$⊢\left(C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}=C\cap \left({\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}\right)$$
34	32 33	eqtr4i	$$⊢C\cap K=\left(C\cap {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\cap \left\{f|{finSupp}_{0_R}\left(f\right)\right\}$$
35	24 28 34	3eqtr4g	$$⊢\phi \to B=C\cap K$$