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 
|- ( ph -> P e. Prob )
dstrvprob.2 
|- ( ph -> X e. ( rRndVar ` P ) )
dstrvprob.3 
|- ( ph -> D = ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) )
Assertion dstrvprob 
|- ( ph -> D e. Prob )

Proof

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