Theorem mvrvalind

Description: Value of the generating elements of the power series structure, expressed using the indicator function. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	mvrvalind.1	$$⊢V=I\mathrm{mVar}R$$
	mvrvalind.2	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mvrvalind.3	$$⊢\underset{\dot{}}{0}=0_R$$
	mvrvalind.4	$$⊢\underset{\dot{}}{1}=1_R$$
	mvrvalind.5	$$⊢\phi \to I\in W$$
	mvrvalind.6	$$⊢\phi \to R\in Y$$
	mvrvalind.7	$$⊢\phi \to X\in I$$
	mvrvalind.8	$$⊢\phi \to F\in D$$
	mvrvalind.9	$$⊢A={𝟙}_I\left(\left\{X\right\}\right)$$
Assertion	mvrvalind	$$⊢\phi \to V\left(X\right)\left(F\right)=if\left(F=A,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mvrvalind.1	$$⊢V=I\mathrm{mVar}R$$
2		mvrvalind.2	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mvrvalind.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		mvrvalind.4	$$⊢\underset{\dot{}}{1}=1_R$$
5		mvrvalind.5	$$⊢\phi \to I\in W$$
6		mvrvalind.6	$$⊢\phi \to R\in Y$$
7		mvrvalind.7	$$⊢\phi \to X\in I$$
8		mvrvalind.8	$$⊢\phi \to F\in D$$
9		mvrvalind.9	$$⊢A={𝟙}_I\left(\left\{X\right\}\right)$$
10	1 2 3 4 5 6 7 8	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)$$
11	9	a1i	$$⊢\phi \to A={𝟙}_I\left(\left\{X\right\}\right)$$
12	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
13		indval	$$⊢\left(I\in W\wedge \left\{X\right\}\subseteq I\right)\to {𝟙}_I\left(\left\{X\right\}\right)=\left(y\in I⟼if\left(y\in \left\{X\right\},1,0\right)\right)$$
14	5 12 13	syl2anc	$$⊢\phi \to {𝟙}_I\left(\left\{X\right\}\right)=\left(y\in I⟼if\left(y\in \left\{X\right\},1,0\right)\right)$$
15		velsn	$$⊢y\in \left\{X\right\}\leftrightarrow y=X$$
16	15	a1i	$$⊢\phi \to \left(y\in \left\{X\right\}\leftrightarrow y=X\right)$$
17	16	ifbid	$$⊢\phi \to if\left(y\in \left\{X\right\},1,0\right)=if\left(y=X,1,0\right)$$
18	17	mpteq2dv	$$⊢\phi \to \left(y\in I⟼if\left(y\in \left\{X\right\},1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
19	11 14 18	3eqtrd	$$⊢\phi \to A=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
20	19	eqeq2d	$$⊢\phi \to \left(F=A\leftrightarrow F=\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
21	20	ifbid	$$⊢\phi \to if\left(F=A,\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)$$
22	10 21	eqtr4d	$$⊢\phi \to V\left(X\right)\left(F\right)=if\left(F=A,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$