Metamath Proof Explorer


Theorem dstrvval

Description: The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017)

Ref Expression
Hypotheses dstrvprob.1 ( 𝜑𝑃 ∈ Prob )
dstrvprob.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
dstrvprob.3 ( 𝜑𝐷 = ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) )
dstrvval.1 ( 𝜑𝐴 ∈ 𝔅 )
Assertion dstrvval ( 𝜑 → ( 𝐷𝐴 ) = ( 𝑃 ‘ ( 𝑋𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dstrvprob.1 ( 𝜑𝑃 ∈ Prob )
2 dstrvprob.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 dstrvprob.3 ( 𝜑𝐷 = ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) )
4 dstrvval.1 ( 𝜑𝐴 ∈ 𝔅 )
5 3 fveq1d ( 𝜑 → ( 𝐷𝐴 ) = ( ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) )
6 oveq2 ( 𝑎 = 𝐴 → ( 𝑋RV/𝑐 E 𝑎 ) = ( 𝑋RV/𝑐 E 𝐴 ) )
7 6 fveq2d ( 𝑎 = 𝐴 → ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) = ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝐴 ) ) )
8 eqid ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) = ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) )
9 fvex ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝐴 ) ) ∈ V
10 7 8 9 fvmpt ( 𝐴 ∈ 𝔅 → ( ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝐴 ) ) )
11 4 10 syl ( 𝜑 → ( ( 𝑎 ∈ 𝔅 ↦ ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝐴 ) ) )
12 1 2 4 orvcelval ( 𝜑 → ( 𝑋RV/𝑐 E 𝐴 ) = ( 𝑋𝐴 ) )
13 12 fveq2d ( 𝜑 → ( 𝑃 ‘ ( 𝑋RV/𝑐 E 𝐴 ) ) = ( 𝑃 ‘ ( 𝑋𝐴 ) ) )
14 5 11 13 3eqtrd ( 𝜑 → ( 𝐷𝐴 ) = ( 𝑃 ‘ ( 𝑋𝐴 ) ) )