Theorem mvrid

Description: The X i -th coefficient of the term X i is 1 . (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$$
Assertion	mvrid	$$⊢\phi \to V\left(X\right)\left(\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\underset{\dot{}}{1}$$

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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9	2	snifpsrbag	$$⊢\left(I\in W\wedge 1\in {\mathbb{N}}_0\right)\to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in D$$
10	5 8 9	sylancl	$$⊢\phi \to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in D$$
11	1 2 3 4 5 6 7 10	mvrval2	$$⊢\phi \to V\left(X\right)\left(\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=if\left(\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
12		eqid	$$⊢\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
13	12	iftruei	$$⊢if\left(\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
14	11 13	eqtrdi	$$⊢\phi \to V\left(X\right)\left(\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\underset{\dot{}}{1}$$