Theorem resspsrbas

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

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

Proof

Step	Hyp	Ref	Expression
1		resspsr.s	$$⊢S=I\mathrm{mPwSer}R$$
2		resspsr.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		resspsr.u	$$⊢U=I\mathrm{mPwSer}H$$
4		resspsr.b	$$⊢B={\mathrm{Base}}_U$$
5		resspsr.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
6		resspsr.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
7		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
8	2	subrgbas	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T={\mathrm{Base}}_H$$
9	6 8	syl	$$⊢\phi \to T={\mathrm{Base}}_H$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	10	subrgss	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T\subseteq {\mathrm{Base}}_R$$
12	6 11	syl	$$⊢\phi \to T\subseteq {\mathrm{Base}}_R$$
13	9 12	eqsstrrd	$$⊢\phi \to {\mathrm{Base}}_H\subseteq {\mathrm{Base}}_R$$
14	13	adantr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_H\subseteq {\mathrm{Base}}_R$$
15		mapss	$$⊢\left({\mathrm{Base}}_R\in \mathrm{V}\wedge {\mathrm{Base}}_H\subseteq {\mathrm{Base}}_R\right)\to {{\mathrm{Base}}_H}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\subseteq {{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
16	7 14 15	sylancr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {{\mathrm{Base}}_H}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\subseteq {{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
17		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
18		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
19		simpr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to I\in \mathrm{V}$$
20	3 17 18 4 19	psrbas	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to B={{\mathrm{Base}}_H}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
21		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
22	1 10 18 21 19	psrbas	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_S={{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
23	16 20 22	3sstr4d	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to B\subseteq {\mathrm{Base}}_S$$
24		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
25	24	ovprc1	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPwSer}H=\varnothing$$
26	3 25	syl5eq	$$⊢\neg I\in \mathrm{V}\to U=\varnothing$$
27	26	adantl	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to U=\varnothing$$
28	27	fveq2d	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to {\mathrm{Base}}_U={\mathrm{Base}}_{\varnothing }$$
29		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
30	28 4 29	3eqtr4g	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to B=\varnothing$$
31		0ss	$$⊢\varnothing \subseteq {\mathrm{Base}}_S$$
32	30 31	eqsstrdi	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to B\subseteq {\mathrm{Base}}_S$$
33	23 32	pm2.61dan	$$⊢\phi \to B\subseteq {\mathrm{Base}}_S$$
34	5 21	ressbas2	$$⊢B\subseteq {\mathrm{Base}}_S\to B={\mathrm{Base}}_P$$
35	33 34	syl	$$⊢\phi \to B={\mathrm{Base}}_P$$