Theorem mvrcl

Description: A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mvrcl.s	$$⊢P=I\mathrm{mPoly}R$$
	mvrcl.v	$$⊢V=I\mathrm{mVar}R$$
	mvrcl.b	$$⊢B={\mathrm{Base}}_P$$
	mvrcl.i	$$⊢\phi \to I\in W$$
	mvrcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mvrcl.x	$$⊢\phi \to X\in I$$
Assertion	mvrcl	$$⊢\phi \to V\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		mvrcl.s	$$⊢P=I\mathrm{mPoly}R$$
2		mvrcl.v	$$⊢V=I\mathrm{mVar}R$$
3		mvrcl.b	$$⊢B={\mathrm{Base}}_P$$
4		mvrcl.i	$$⊢\phi \to I\in W$$
5		mvrcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mvrcl.x	$$⊢\phi \to X\in I$$
7		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9	7 2 8 4 5 6	mvrcl2	$$⊢\phi \to V\left(X\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
10		fvexd	$$⊢\phi \to V\left(X\right)\in \mathrm{V}$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		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\}$$
13	7 11 12 8 9	psrelbas	$$⊢\phi \to V\left(X\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
14	13	ffund	$$⊢\phi \to \mathrm{Fun}V\left(X\right)$$
15		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
16		snfi	$$⊢\left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\in \mathrm{Fin}$$
17	16	a1i	$$⊢\phi \to \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\in \mathrm{Fin}$$
18		eqid	$$⊢0_R=0_R$$
19		eqid	$$⊢1_R=1_R$$
20	4	adantr	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to I\in W$$
21	5	adantr	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to R\in \mathrm{Ring}$$
22	6	adantr	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to X\in I$$
23		eldifsn	$$⊢x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\leftrightarrow \left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge x\ne \left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
24	23	bilani	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to \left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge x\ne \left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
25	24	simpld	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
26	2 12 18 19 20 21 22 25	mvrval2	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to V\left(X\right)\left(x\right)=if\left(x=\left(y\in I⟼if\left(y=X,1,0\right)\right),1_R,0_R\right)$$
27	24	simprd	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to x\ne \left(y\in I⟼if\left(y=X,1,0\right)\right)$$
28	27	neneqd	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to \neg x=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
29	28	iffalsed	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to if\left(x=\left(y\in I⟼if\left(y=X,1,0\right)\right),1_R,0_R\right)=0_R$$
30	26 29	eqtrd	$$⊢\left(\phi \wedge x\in \left(\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to V\left(X\right)\left(x\right)=0_R$$
31	13 30	suppss	$$⊢\phi \to V\left(X\right)\mathrm{supp}{0}_R\subseteq \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}$$
32		suppssfifsupp	$$⊢\left(\left(V\left(X\right)\in \mathrm{V}\wedge \mathrm{Fun}V\left(X\right)\wedge 0_R\in \mathrm{V}\right)\wedge \left(\left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\in \mathrm{Fin}\wedge V\left(X\right)\mathrm{supp}{0}_R\subseteq \left\{\left(y\in I⟼if\left(y=X,1,0\right)\right)\right\}\right)\right)\to {finSupp}_{0_R}\left(V\left(X\right)\right)$$
33	10 14 15 17 31 32	syl32anc	$$⊢\phi \to {finSupp}_{0_R}\left(V\left(X\right)\right)$$
34	1 7 8 18 3	mplelbas	$$⊢V\left(X\right)\in B\leftrightarrow \left(V\left(X\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{0_R}\left(V\left(X\right)\right)\right)$$
35	9 33 34	sylanbrc	$$⊢\phi \to V\left(X\right)\in B$$