Description: Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | probfinmeasb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | measdivcst | |
|
2 | measfn | |
|
3 | 2 | adantr | |
4 | measbase | |
|
5 | 4 | adantr | |
6 | simpr | |
|
7 | 3 5 6 | ofcfn | |
8 | 7 | fndmd | |
9 | 8 | fveq2d | |
10 | 1 9 | eleqtrrd | |
11 | measbasedom | |
|
12 | 10 11 | sylibr | |
13 | 8 | unieqd | |
14 | 13 | fveq2d | |
15 | unielsiga | |
|
16 | 5 15 | syl | |
17 | eqidd | |
|
18 | 3 5 6 17 | ofcval | |
19 | 16 18 | mpdan | |
20 | rpre | |
|
21 | rpne0 | |
|
22 | xdivid | |
|
23 | 20 21 22 | syl2anc | |
24 | 23 | adantl | |
25 | 14 19 24 | 3eqtrd | |
26 | elprob | |
|
27 | 12 25 26 | sylanbrc | |