Theorem mvrf

Description: The power series variable function is a function from the index set to elements of the power series structure representing X i for each i . (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	mvrf.s	$$⊢S=I\mathrm{mPwSer}R$$
	mvrf.v	$$⊢V=I\mathrm{mVar}R$$
	mvrf.b	$$⊢B={\mathrm{Base}}_S$$
	mvrf.i	$$⊢\phi \to I\in W$$
	mvrf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mvrf	$$⊢\phi \to V:I⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mvrf.s	$$⊢S=I\mathrm{mPwSer}R$$
2		mvrf.v	$$⊢V=I\mathrm{mVar}R$$
3		mvrf.b	$$⊢B={\mathrm{Base}}_S$$
4		mvrf.i	$$⊢\phi \to I\in W$$
5		mvrf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		eqid	$$⊢0_R=0_R$$
8		eqid	$$⊢1_R=1_R$$
9	2 6 7 8 4 5	mvrfval	$$⊢\phi \to V=\left(x\in I⟼\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	10 8	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
12	5 11	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
13	10 7	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
14	5 13	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
15	12 14	ifcld	$$⊢\phi \to if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\in {\mathrm{Base}}_R$$
16	15	ad2antrr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\in {\mathrm{Base}}_R$$
17	16	fmpttd	$$⊢\left(\phi \wedge x\in I\right)\to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
18		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
19		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
20	19	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
21	18 20	elmap	$$⊢\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right)\in \left({{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\leftrightarrow \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
22	17 21	sylibr	$$⊢\left(\phi \wedge x\in I\right)\to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right)\in \left({{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
23	1 10 6 3 4	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
24	23	adantr	$$⊢\left(\phi \wedge x\in I\right)\to B={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
25	22 24	eleqtrrd	$$⊢\left(\phi \wedge x\in I\right)\to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),1_R,0_R\right)\right)\in B$$
26	9 25	fmpt3d	$$⊢\phi \to V:I⟶B$$