Metamath Proof Explorer

Theorem probmeasb

Description: Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion probmeasb 
|- ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. Prob )

Proof

Step Hyp Ref Expression
1 measinb 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( y e. S |-> ( M ` ( y i^i A ) ) ) e. ( measures ` S ) )
2 measdivcstALTV 
 |-  ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) e. ( measures ` S ) /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) /e ( M ` A ) ) ) e. ( measures ` S ) )
3 1 2 stoic3 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) /e ( M ` A ) ) ) e. ( measures ` S ) )
4 eqidd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( y e. S |-> ( M ` ( y i^i A ) ) ) = ( y e. S |-> ( M ` ( y i^i A ) ) ) )
5 simpr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) /\ y = x ) -> y = x )
6 5 ineq1d 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) /\ y = x ) -> ( y i^i A ) = ( x i^i A ) )
7 6 fveq2d 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) /\ y = x ) -> ( M ` ( y i^i A ) ) = ( M ` ( x i^i A ) ) )
8 simpr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> x e. S )
9 simp1 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> M e. ( measures ` S ) )
10 9 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> M e. ( measures ` S ) )
11 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
12 10 11 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> S e. U. ran sigAlgebra )
13 simp2 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> A e. S )
14 13 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> A e. S )
15 inelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ x e. S /\ A e. S ) -> ( x i^i A ) e. S )
16 12 8 14 15 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( x i^i A ) e. S )
17 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( x i^i A ) e. S ) -> ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) )
18 10 16 17 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) )
19 4 7 8 18 fvmptd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) = ( M ` ( x i^i A ) ) )
20 19 oveq1d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) /e ( M ` A ) ) = ( ( M ` ( x i^i A ) ) /e ( M ` A ) ) )
21 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
22 21 18 sselid 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` ( x i^i A ) ) e. RR* )
23 simp3 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( M ` A ) e. RR+ )
24 23 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` A ) e. RR+ )
25 24 rpred 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` A ) e. RR )
26 0xr 
 |-  0 e. RR*
27 pnfxr 
 |-  +oo e. RR*
28 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) ) -> 0 <_ ( M ` ( x i^i A ) ) )
29 26 27 28 mp3an12 
 |-  ( ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) -> 0 <_ ( M ` ( x i^i A ) ) )
30 18 29 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> 0 <_ ( M ` ( x i^i A ) ) )
31 inss2 
 |-  ( x i^i A ) C_ A
32 31 a1i 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( x i^i A ) C_ A )
33 10 16 14 32 measssd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` ( x i^i A ) ) <_ ( M ` A ) )
34 xrrege0 
 |-  ( ( ( ( M ` ( x i^i A ) ) e. RR* /\ ( M ` A ) e. RR ) /\ ( 0 <_ ( M ` ( x i^i A ) ) /\ ( M ` ( x i^i A ) ) <_ ( M ` A ) ) ) -> ( M ` ( x i^i A ) ) e. RR )
35 22 25 30 33 34 syl22anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` ( x i^i A ) ) e. RR )
36 24 rpne0d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( M ` A ) =/= 0 )
37 rexdiv 
 |-  ( ( ( M ` ( x i^i A ) ) e. RR /\ ( M ` A ) e. RR /\ ( M ` A ) =/= 0 ) -> ( ( M ` ( x i^i A ) ) /e ( M ` A ) ) = ( ( M ` ( x i^i A ) ) / ( M ` A ) ) )
38 35 25 36 37 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( ( M ` ( x i^i A ) ) /e ( M ` A ) ) = ( ( M ` ( x i^i A ) ) / ( M ` A ) ) )
39 20 38 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) /e ( M ` A ) ) = ( ( M ` ( x i^i A ) ) / ( M ` A ) ) )
40 39 mpteq2dva 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( ( y e. S |-> ( M ` ( y i^i A ) ) ) ` x ) /e ( M ` A ) ) ) = ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) )
41 35 24 rerpdivcld 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x e. S ) -> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) e. RR )
42 41 ralrimiva 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> A. x e. S ( ( M ` ( x i^i A ) ) / ( M ` A ) ) e. RR )
43 dmmptg 
 |-  ( A. x e. S ( ( M ` ( x i^i A ) ) / ( M ` A ) ) e. RR -> dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) = S )
44 42 43 syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) = S )
45 44 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( measures ` dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) = ( measures ` S ) )
46 45 eqcomd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( measures ` S ) = ( measures ` dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) )
47 3 40 46 3eltr3d 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. ( measures ` dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) )
48 measbasedom 
 |-  ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. U. ran measures <-> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. ( measures ` dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) )
49 47 48 sylibr 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. U. ran measures )
50 44 unieqd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> U. dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) = U. S )
51 50 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ` U. dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) = ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ` U. S ) )
52 eqidd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) = ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) )
53 23 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( M ` A ) e. RR+ )
54 53 rpcnd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( M ` A ) e. CC )
55 23 rpne0d 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( M ` A ) =/= 0 )
56 55 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( M ` A ) =/= 0 )
57 simpr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> x = U. S )
58 57 ineq1d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( x i^i A ) = ( U. S i^i A ) )
59 incom 
 |-  ( U. S i^i A ) = ( A i^i U. S )
60 elssuni 
 |-  ( A e. S -> A C_ U. S )
61 df-ss 
 |-  ( A C_ U. S <-> ( A i^i U. S ) = A )
62 60 61 sylib 
 |-  ( A e. S -> ( A i^i U. S ) = A )
63 59 62 syl5eq 
 |-  ( A e. S -> ( U. S i^i A ) = A )
64 13 63 syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( U. S i^i A ) = A )
65 64 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( U. S i^i A ) = A )
66 58 65 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( x i^i A ) = A )
67 66 fveq2d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( M ` ( x i^i A ) ) = ( M ` A ) )
68 54 56 67 diveq1bd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) /\ x = U. S ) -> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) = 1 )
69 sgon 
 |-  ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )
70 baselsiga 
 |-  ( S e. ( sigAlgebra ` U. S ) -> U. S e. S )
71 9 11 69 70 4syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> U. S e. S )
72 1red 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> 1 e. RR )
73 52 68 71 72 fvmptd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ` U. S ) = 1 )
74 51 73 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ` U. dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) = 1 )
75 elprob 
 |-  ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. Prob <-> ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. U. ran measures /\ ( ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ` U. dom ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) ) = 1 ) )
76 49 74 75 sylanbrc 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. Prob )