Metamath Proof Explorer


Theorem dstrvprob

Description: The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval ). (Contributed by Thierry Arnoux, 10-Feb-2017)

Ref Expression
Hypotheses dstrvprob.1 φ P Prob
dstrvprob.2 φ X RndVar P
dstrvprob.3 φ D = a 𝔅 P X E RV/c a
Assertion dstrvprob φ D Prob

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 1 adantr φ a 𝔅 P Prob
5 2 adantr φ a 𝔅 X RndVar P
6 simpr φ a 𝔅 a 𝔅
7 4 5 6 orvcelel φ a 𝔅 X E RV/c a dom P
8 prob01 P Prob X E RV/c a dom P P X E RV/c a 0 1
9 4 7 8 syl2anc φ a 𝔅 P X E RV/c a 0 1
10 elunitrn P X E RV/c a 0 1 P X E RV/c a
11 10 rexrd P X E RV/c a 0 1 P X E RV/c a *
12 elunitge0 P X E RV/c a 0 1 0 P X E RV/c a
13 elxrge0 P X E RV/c a 0 +∞ P X E RV/c a * 0 P X E RV/c a
14 11 12 13 sylanbrc P X E RV/c a 0 1 P X E RV/c a 0 +∞
15 9 14 syl φ a 𝔅 P X E RV/c a 0 +∞
16 3 15 fmpt3d φ D : 𝔅 0 +∞
17 simpr φ a = a =
18 17 oveq2d φ a = X E RV/c a = X E RV/c
19 18 fveq2d φ a = P X E RV/c a = P X E RV/c
20 brsigarn 𝔅 sigAlgebra
21 elrnsiga 𝔅 sigAlgebra 𝔅 ran sigAlgebra
22 0elsiga 𝔅 ran sigAlgebra 𝔅
23 20 21 22 mp2b 𝔅
24 23 a1i φ 𝔅
25 1 2 24 orvcelel φ X E RV/c dom P
26 1 25 probvalrnd φ P X E RV/c
27 3 19 24 26 fvmptd φ D = P X E RV/c
28 1 2 24 orvcelval φ X E RV/c = X -1
29 28 fveq2d φ P X E RV/c = P X -1
30 ima0 X -1 =
31 30 fveq2i P X -1 = P
32 probnul P Prob P = 0
33 1 32 syl φ P = 0
34 31 33 syl5eq φ P X -1 = 0
35 27 29 34 3eqtrd φ D = 0
36 1 2 rrvvf φ X : dom P
37 36 ad2antrr φ x 𝒫 𝔅 x ω Disj a x a X : dom P
38 37 ffund φ x 𝒫 𝔅 x ω Disj a x a Fun X
39 unipreima Fun X X -1 x = a x X -1 a
40 39 fveq2d Fun X P X -1 x = P a x X -1 a
41 38 40 syl φ x 𝒫 𝔅 x ω Disj a x a P X -1 x = P a x X -1 a
42 1 ad2antrr φ x 𝒫 𝔅 x ω Disj a x a P Prob
43 domprobmeas P Prob P measures dom P
44 42 43 syl φ x 𝒫 𝔅 x ω Disj a x a P measures dom P
45 nfv a φ x 𝒫 𝔅
46 nfv a x ω
47 nfdisj1 a Disj a x a
48 46 47 nfan a x ω Disj a x a
49 45 48 nfan a φ x 𝒫 𝔅 x ω Disj a x a
50 simplll φ x 𝒫 𝔅 x ω Disj a x a a x φ
51 simpr φ x 𝒫 𝔅 x ω Disj a x a a x a x
52 simpllr φ x 𝒫 𝔅 x ω Disj a x a a x x 𝒫 𝔅
53 elelpwi a x x 𝒫 𝔅 a 𝔅
54 51 52 53 syl2anc φ x 𝒫 𝔅 x ω Disj a x a a x a 𝔅
55 1 2 rrvfinvima φ a 𝔅 X -1 a dom P
56 55 r19.21bi φ a 𝔅 X -1 a dom P
57 50 54 56 syl2anc φ x 𝒫 𝔅 x ω Disj a x a a x X -1 a dom P
58 57 ex φ x 𝒫 𝔅 x ω Disj a x a a x X -1 a dom P
59 49 58 ralrimi φ x 𝒫 𝔅 x ω Disj a x a a x X -1 a dom P
60 simprl φ x 𝒫 𝔅 x ω Disj a x a x ω
61 simprr φ x 𝒫 𝔅 x ω Disj a x a Disj a x a
62 disjpreima Fun X Disj a x a Disj a x X -1 a
63 38 61 62 syl2anc φ x 𝒫 𝔅 x ω Disj a x a Disj a x X -1 a
64 measvuni P measures dom P a x X -1 a dom P x ω Disj a x X -1 a P a x X -1 a = * a x P X -1 a
65 44 59 60 63 64 syl112anc φ x 𝒫 𝔅 x ω Disj a x a P a x X -1 a = * a x P X -1 a
66 41 65 eqtrd φ x 𝒫 𝔅 x ω Disj a x a P X -1 x = * a x P X -1 a
67 2 ad2antrr φ x 𝒫 𝔅 x ω Disj a x a X RndVar P
68 3 ad2antrr φ x 𝒫 𝔅 x ω Disj a x a D = a 𝔅 P X E RV/c a
69 20 21 mp1i φ x 𝒫 𝔅 x ω Disj a x a 𝔅 ran sigAlgebra
70 simplr φ x 𝒫 𝔅 x ω Disj a x a x 𝒫 𝔅
71 sigaclcu 𝔅 ran sigAlgebra x 𝒫 𝔅 x ω x 𝔅
72 69 70 60 71 syl3anc φ x 𝒫 𝔅 x ω Disj a x a x 𝔅
73 42 67 68 72 dstrvval φ x 𝒫 𝔅 x ω Disj a x a D x = P X -1 x
74 3 9 fvmpt2d φ a 𝔅 D a = P X E RV/c a
75 50 54 74 syl2anc φ x 𝒫 𝔅 x ω Disj a x a a x D a = P X E RV/c a
76 42 adantr φ x 𝒫 𝔅 x ω Disj a x a a x P Prob
77 67 adantr φ x 𝒫 𝔅 x ω Disj a x a a x X RndVar P
78 76 77 54 orvcelval φ x 𝒫 𝔅 x ω Disj a x a a x X E RV/c a = X -1 a
79 78 fveq2d φ x 𝒫 𝔅 x ω Disj a x a a x P X E RV/c a = P X -1 a
80 75 79 eqtrd φ x 𝒫 𝔅 x ω Disj a x a a x D a = P X -1 a
81 80 ex φ x 𝒫 𝔅 x ω Disj a x a a x D a = P X -1 a
82 49 81 ralrimi φ x 𝒫 𝔅 x ω Disj a x a a x D a = P X -1 a
83 49 82 esumeq2d φ x 𝒫 𝔅 x ω Disj a x a * a x D a = * a x P X -1 a
84 66 73 83 3eqtr4d φ x 𝒫 𝔅 x ω Disj a x a D x = * a x D a
85 84 ex φ x 𝒫 𝔅 x ω Disj a x a D x = * a x D a
86 85 ralrimiva φ x 𝒫 𝔅 x ω Disj a x a D x = * a x D a
87 ismeas 𝔅 ran sigAlgebra D measures 𝔅 D : 𝔅 0 +∞ D = 0 x 𝒫 𝔅 x ω Disj a x a D x = * a x D a
88 20 21 87 mp2b D measures 𝔅 D : 𝔅 0 +∞ D = 0 x 𝒫 𝔅 x ω Disj a x a D x = * a x D a
89 16 35 86 88 syl3anbrc φ D measures 𝔅
90 3 dmeqd φ dom D = dom a 𝔅 P X E RV/c a
91 15 ralrimiva φ a 𝔅 P X E RV/c a 0 +∞
92 dmmptg a 𝔅 P X E RV/c a 0 +∞ dom a 𝔅 P X E RV/c a = 𝔅
93 91 92 syl φ dom a 𝔅 P X E RV/c a = 𝔅
94 90 93 eqtrd φ dom D = 𝔅
95 94 fveq2d φ measures dom D = measures 𝔅
96 89 95 eleqtrrd φ D measures dom D
97 measbasedom D ran measures D measures dom D
98 96 97 sylibr φ D ran measures
99 94 unieqd φ dom D = 𝔅
100 unibrsiga 𝔅 =
101 99 100 eqtrdi φ dom D =
102 101 fveq2d φ D dom D = D
103 simpr φ a = a =
104 103 oveq2d φ a = X E RV/c a = X E RV/c
105 baselsiga 𝔅 sigAlgebra 𝔅
106 20 105 mp1i φ 𝔅
107 1 2 106 orvcelval φ X E RV/c = X -1
108 107 adantr φ a = X E RV/c = X -1
109 104 108 eqtrd φ a = X E RV/c a = X -1
110 109 fveq2d φ a = P X E RV/c a = P X -1
111 fimacnv X : dom P X -1 = dom P
112 36 111 syl φ X -1 = dom P
113 112 fveq2d φ P X -1 = P dom P
114 probtot P Prob P dom P = 1
115 1 114 syl φ P dom P = 1
116 113 115 eqtrd φ P X -1 = 1
117 116 adantr φ a = P X -1 = 1
118 110 117 eqtrd φ a = P X E RV/c a = 1
119 1red φ 1
120 3 118 106 119 fvmptd φ D = 1
121 102 120 eqtrd φ D dom D = 1
122 elprob D Prob D ran measures D dom D = 1
123 98 121 122 sylanbrc φ D Prob