Metamath Proof Explorer


Theorem indfval

Description: Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017)

Ref Expression
Assertion indfval ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋𝐴 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 indval ( ( 𝑂𝑉𝐴𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥𝑂 ↦ if ( 𝑥𝐴 , 1 , 0 ) ) )
2 1 3adant3 ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥𝑂 ↦ if ( 𝑥𝐴 , 1 , 0 ) ) )
3 simpr ( ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
4 3 eleq1d ( ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) ∧ 𝑥 = 𝑋 ) → ( 𝑥𝐴𝑋𝐴 ) )
5 4 ifbid ( ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥𝐴 , 1 , 0 ) = if ( 𝑋𝐴 , 1 , 0 ) )
6 simp3 ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) → 𝑋𝑂 )
7 1re 1 ∈ ℝ
8 0re 0 ∈ ℝ
9 7 8 ifcli if ( 𝑋𝐴 , 1 , 0 ) ∈ ℝ
10 9 a1i ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) → if ( 𝑋𝐴 , 1 , 0 ) ∈ ℝ )
11 2 5 6 10 fvmptd ( ( 𝑂𝑉𝐴𝑂𝑋𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋𝐴 , 1 , 0 ) )