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 φ P Prob
dstrvprob.2 φ X RndVar P
dstrvprob.3 φ D = a 𝔅 P X E RV/c a
dstrvval.1 φ A 𝔅
Assertion dstrvval φ D A = P X -1 A

Proof

Step Hyp Ref Expression
1 dstrvprob.1 φ P Prob
2 dstrvprob.2 φ X RndVar P
3 dstrvprob.3 φ D = a 𝔅 P X E RV/c a
4 dstrvval.1 φ A 𝔅
5 3 fveq1d φ D A = a 𝔅 P X E RV/c a A
6 oveq2 a = A X E RV/c a = X E RV/c A
7 6 fveq2d a = A P X E RV/c a = P X E RV/c A
8 eqid a 𝔅 P X E RV/c a = a 𝔅 P X E RV/c a
9 fvex P X E RV/c A V
10 7 8 9 fvmpt A 𝔅 a 𝔅 P X E RV/c a A = P X E RV/c A
11 4 10 syl φ a 𝔅 P X E RV/c a A = P X E RV/c A
12 1 2 4 orvcelval φ X E RV/c A = X -1 A
13 12 fveq2d φ P X E RV/c A = P X -1 A
14 5 11 13 3eqtrd φ D A = P X -1 A