Metamath Proof Explorer


Theorem probfinmeasb

Description: Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017)

Ref Expression
Assertion probfinmeasb MmeasuresSMS+Mfc÷𝑒MSProb

Proof

Step Hyp Ref Expression
1 measdivcst MmeasuresSMS+Mfc÷𝑒MSmeasuresS
2 measfn MmeasuresSMFnS
3 2 adantr MmeasuresSMS+MFnS
4 measbase MmeasuresSSransigAlgebra
5 4 adantr MmeasuresSMS+SransigAlgebra
6 simpr MmeasuresSMS+MS+
7 3 5 6 ofcfn MmeasuresSMS+Mfc÷𝑒MSFnS
8 7 fndmd MmeasuresSMS+domMfc÷𝑒MS=S
9 8 fveq2d MmeasuresSMS+measuresdomMfc÷𝑒MS=measuresS
10 1 9 eleqtrrd MmeasuresSMS+Mfc÷𝑒MSmeasuresdomMfc÷𝑒MS
11 measbasedom Mfc÷𝑒MSranmeasuresMfc÷𝑒MSmeasuresdomMfc÷𝑒MS
12 10 11 sylibr MmeasuresSMS+Mfc÷𝑒MSranmeasures
13 8 unieqd MmeasuresSMS+domMfc÷𝑒MS=S
14 13 fveq2d MmeasuresSMS+Mfc÷𝑒MSdomMfc÷𝑒MS=Mfc÷𝑒MSS
15 unielsiga SransigAlgebraSS
16 5 15 syl MmeasuresSMS+SS
17 eqidd MmeasuresSMS+SSMS=MS
18 3 5 6 17 ofcval MmeasuresSMS+SSMfc÷𝑒MSS=MS÷𝑒MS
19 16 18 mpdan MmeasuresSMS+Mfc÷𝑒MSS=MS÷𝑒MS
20 rpre MS+MS
21 rpne0 MS+MS0
22 xdivid MSMS0MS÷𝑒MS=1
23 20 21 22 syl2anc MS+MS÷𝑒MS=1
24 23 adantl MmeasuresSMS+MS÷𝑒MS=1
25 14 19 24 3eqtrd MmeasuresSMS+Mfc÷𝑒MSdomMfc÷𝑒MS=1
26 elprob Mfc÷𝑒MSProbMfc÷𝑒MSranmeasuresMfc÷𝑒MSdomMfc÷𝑒MS=1
27 12 25 26 sylanbrc MmeasuresSMS+Mfc÷𝑒MSProb