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 mVar R )
	mvrvalind.2	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	mvrvalind.3	|- .0. = ( 0g ` R )
	mvrvalind.4	|- .1. = ( 1r ` R )
	mvrvalind.5	|- ( ph -> I e. W )
	mvrvalind.6	|- ( ph -> R e. Y )
	mvrvalind.7	|- ( ph -> X e. I )
	mvrvalind.8	|- ( ph -> F e. D )
	mvrvalind.9	|- A = ( ( _Ind ` I ) ` { X } )
Assertion	mvrvalind	|- ( ph -> ( ( V ` X ) ` F ) = if ( F = A , .1. , .0. ) )

Proof

Step	Hyp	Ref	Expression
1		mvrvalind.1	|- V = ( I mVar R )
2		mvrvalind.2	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
3		mvrvalind.3	|- .0. = ( 0g ` R )
4		mvrvalind.4	|- .1. = ( 1r ` R )
5		mvrvalind.5	|- ( ph -> I e. W )
6		mvrvalind.6	|- ( ph -> R e. Y )
7		mvrvalind.7	|- ( ph -> X e. I )
8		mvrvalind.8	|- ( ph -> F e. D )
9		mvrvalind.9	|- A = ( ( _Ind ` I ) ` { X } )
10	1 2 3 4 5 6 7 8	mvrval2	|- ( ph -> ( ( V ` X ) ` F ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
11	9	a1i	|- ( ph -> A = ( ( _Ind ` I ) ` { X } ) )
12	7	snssd	|- ( ph -> { X } C_ I )
13		indval	|- ( ( I e. W /\ { X } C_ I ) -> ( ( _Ind ` I ) ` { X } ) = ( y e. I |-> if ( y e. { X } , 1 , 0 ) ) )
14	5 12 13	syl2anc	|- ( ph -> ( ( _Ind ` I ) ` { X } ) = ( y e. I |-> if ( y e. { X } , 1 , 0 ) ) )
15		velsn	|- ( y e. { X } <-> y = X )
16	15	a1i	|- ( ph -> ( y e. { X } <-> y = X ) )
17	16	ifbid	|- ( ph -> if ( y e. { X } , 1 , 0 ) = if ( y = X , 1 , 0 ) )
18	17	mpteq2dv	|- ( ph -> ( y e. I |-> if ( y e. { X } , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) )
19	11 14 18	3eqtrd	|- ( ph -> A = ( y e. I |-> if ( y = X , 1 , 0 ) ) )
20	19	eqeq2d	|- ( ph -> ( F = A <-> F = ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
21	20	ifbid	|- ( ph -> if ( F = A , .1. , .0. ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
22	10 21	eqtr4d	|- ( ph -> ( ( V ` X ) ` F ) = if ( F = A , .1. , .0. ) )