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 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ Prob )

Proof

Step Hyp Ref Expression
1 measdivcst ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ( measures ‘ 𝑆 ) )
2 measfn ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 Fn 𝑆 )
3 2 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → 𝑀 Fn 𝑆 )
4 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
5 4 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → 𝑆 ∈ ∪ ran sigAlgebra )
6 simpr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ )
7 3 5 6 ofcfn ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) Fn 𝑆 )
8 7 fndmd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 𝑆 )
9 8 fveq2d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( measures ‘ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = ( measures ‘ 𝑆 ) )
10 1 9 eleqtrrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ( measures ‘ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) )
11 measbasedom ⊢ ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ∪ ran measures ↔ ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ( measures ‘ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) )
12 10 11 sylibr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ∪ ran measures )
13 8 unieqd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ∪ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = ∪ 𝑆 )
14 13 fveq2d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ 𝑆 ) )
15 unielsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆 )
16 5 15 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ∪ 𝑆 ∈ 𝑆 )
17 eqidd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) ∧ ∪ 𝑆 ∈ 𝑆 ) → ( 𝑀 ‘ ∪ 𝑆 ) = ( 𝑀 ‘ ∪ 𝑆 ) )
18 3 5 6 17 ofcval ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) ∧ ∪ 𝑆 ∈ 𝑆 ) → ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ 𝑆 ) = ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
19 16 18 mpdan ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ 𝑆 ) = ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
20 rpre ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ )
21 rpne0 ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( 𝑀 ‘ ∪ 𝑆 ) ≠ 0 )
22 xdivid ⊢ ( ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ ∧ ( 𝑀 ‘ ∪ 𝑆 ) ≠ 0 ) → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
23 20 21 22 syl2anc ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
24 23 adantl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
25 14 19 24 3eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = 1 )
26 elprob ⊢ ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ Prob ↔ ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ∪ ran measures ∧ ( ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ‘ ∪ dom ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = 1 ) )
27 12 25 26 sylanbrc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ Prob )