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 φPProb
dstrvprob.2 φXRndVarP
dstrvprob.3 φD=a𝔅PXERV/ca
dstrvval.1 φA𝔅
Assertion dstrvval φDA=PX-1A

Proof

Step Hyp Ref Expression
1 dstrvprob.1 φPProb
2 dstrvprob.2 φXRndVarP
3 dstrvprob.3 φD=a𝔅PXERV/ca
4 dstrvval.1 φA𝔅
5 3 fveq1d φDA=a𝔅PXERV/caA
6 oveq2 a=AXERV/ca=XERV/cA
7 6 fveq2d a=APXERV/ca=PXERV/cA
8 eqid a𝔅PXERV/ca=a𝔅PXERV/ca
9 fvex PXERV/cAV
10 7 8 9 fvmpt A𝔅a𝔅PXERV/caA=PXERV/cA
11 4 10 syl φa𝔅PXERV/caA=PXERV/cA
12 1 2 4 orvcelval φXERV/cA=X-1A
13 12 fveq2d φPXERV/cA=PX-1A
14 5 11 13 3eqtrd φDA=PX-1A