Theorem mvrf2

Description: The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	mvrf2.p	$$⊢P=I\mathrm{mPoly}R$$
	mvrf2.v	$$⊢V=I\mathrm{mVar}R$$
	mvrf2.b	$$⊢B={\mathrm{Base}}_P$$
	mvrf2.i	$$⊢\phi \to I\in W$$
	mvrf2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mvrf2	$$⊢\phi \to V:I⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mvrf2.p	$$⊢P=I\mathrm{mPoly}R$$
2		mvrf2.v	$$⊢V=I\mathrm{mVar}R$$
3		mvrf2.b	$$⊢B={\mathrm{Base}}_P$$
4		mvrf2.i	$$⊢\phi \to I\in W$$
5		mvrf2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8	6 2 7 4 5	mvrf	$$⊢\phi \to V:I⟶{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9	8	ffnd	$$⊢\phi \to VFnI$$
10	4	adantr	$$⊢\left(\phi \wedge x\in I\right)\to I\in W$$
11	5	adantr	$$⊢\left(\phi \wedge x\in I\right)\to R\in \mathrm{Ring}$$
12		simpr	$$⊢\left(\phi \wedge x\in I\right)\to x\in I$$
13	1 2 3 10 11 12	mvrcl	$$⊢\left(\phi \wedge x\in I\right)\to V\left(x\right)\in B$$
14	13	ralrimiva	$$⊢\phi \to \forall x\in IV\left(x\right)\in B$$
15		ffnfv	$$⊢V:I⟶B\leftrightarrow \left(VFnI\wedge \forall x\in IV\left(x\right)\in B\right)$$
16	9 14 15	sylanbrc	$$⊢\phi \to V:I⟶B$$