Theorem mvrval2

Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	mvrfval.v	$$⊢V=I\mathrm{mVar}R$$
	mvrfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mvrfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mvrfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mvrfval.i	$$⊢\phi \to I\in W$$
	mvrfval.r	$$⊢\phi \to R\in Y$$
	mvrval.x	$$⊢\phi \to X\in I$$
	mvrval2.f	$$⊢\phi \to F\in D$$
Assertion	mvrval2	$$⊢\phi \to V\left(X\right)\left(F\right)=if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mvrfval.v	$$⊢V=I\mathrm{mVar}R$$
2		mvrfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mvrfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mvrfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mvrfval.i	$$⊢\phi \to I\in W$$
6		mvrfval.r	$$⊢\phi \to R\in Y$$
7		mvrval.x	$$⊢\phi \to X\in I$$
8		mvrval2.f	$$⊢\phi \to F\in D$$
9	1 2 3 4 5 6 7	mvrval	$$⊢\phi \to V\left(X\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
10	9	fveq1d	$$⊢\phi \to V\left(X\right)\left(F\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(F\right)$$
11		eqeq1	$$⊢f=F\to \left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right)\leftrightarrow F=\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
12	11	ifbid	$$⊢f=F\to if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
13		eqid	$$⊢\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
14	4	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
15	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
16	14 15	ifex	$$⊢if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
17	12 13 16	fvmpt	$$⊢F\in D\to \left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(F\right)=if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
18	8 17	syl	$$⊢\phi \to \left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(F\right)=if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
19	10 18	eqtrd	$$⊢\phi \to V\left(X\right)\left(F\right)=if\left(F=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$