This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. ) )