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 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ Prob )

Proof

Step Hyp Ref Expression
1 measinb ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )
2 measdivcstALTV ⊢ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )
3 1 2 stoic3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )
4 eqidd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) )
5 simpr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
6 5 ineq1d ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) )
7 6 fveq2d ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
8 simpr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
9 simp1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
10 9 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
11 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
12 10 11 syl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
13 simp2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 𝐴 ∈ 𝑆 )
14 13 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
15 inelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
16 12 8 14 15 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
17 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
18 10 16 17 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
19 4 7 8 18 fvmptd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) = ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
20 19 oveq1d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) )
21 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
22 21 18 sselid ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* )
23 simp3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ )
24 23 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ )
25 24 rpred ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
26 0xr ⊢ 0 ∈ ℝ*
27 pnfxr ⊢ +∞ ∈ ℝ*
28 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
29 26 27 28 mp3an12 ⊢ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
30 18 29 syl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) )
31 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
32 31 a1i ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
33 10 16 14 32 measssd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐴 ) )
34 xrrege0 ⊢ ( ( ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∧ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
35 22 25 30 33 34 syl22anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
36 24 rpne0d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 )
37 rexdiv ⊢ ( ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑀 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) )
38 35 25 36 37 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) )
39 20 38 eqtrd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) )
40 39 mpteq2dva ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) )
41 35 24 rerpdivcld ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ )
42 41 ralrimiva ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ )
43 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = 𝑆 )
44 42 43 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = 𝑆 )
45 44 fveq2d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = ( measures ‘ 𝑆 ) )
46 45 eqcomd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( measures ‘ 𝑆 ) = ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) )
47 3 40 46 3eltr3d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) )
48 measbasedom ⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures ↔ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) )
49 47 48 sylibr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures )
50 44 unieqd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = ∪ 𝑆 )
51 50 fveq2d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ 𝑆 ) )
52 eqidd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) )
53 23 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ )
54 53 rpcnd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℂ )
55 23 rpne0d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 )
56 55 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 )
57 simpr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → 𝑥 = ∪ 𝑆 )
58 57 ineq1d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝑆 ∩ 𝐴 ) )
59 incom ⊢ ( ∪ 𝑆 ∩ 𝐴 ) = ( 𝐴 ∩ ∪ 𝑆 )
60 elssuni ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ⊆ ∪ 𝑆 )
61 df-ss ⊢ ( 𝐴 ⊆ ∪ 𝑆 ↔ ( 𝐴 ∩ ∪ 𝑆 ) = 𝐴 )
62 60 61 sylib ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 ∩ ∪ 𝑆 ) = 𝐴 )
63 59 62 syl5eq ⊢ ( 𝐴 ∈ 𝑆 → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 )
64 13 63 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 )
65 64 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 )
66 58 65 eqtrd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) = 𝐴 )
67 66 fveq2d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) )
68 54 56 67 diveq1bd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) = 1 )
69 sgon ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) )
70 baselsiga ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) → ∪ 𝑆 ∈ 𝑆 )
71 9 11 69 70 4syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∪ 𝑆 ∈ 𝑆 )
72 1red ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 1 ∈ ℝ )
73 52 68 71 72 fvmptd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ 𝑆 ) = 1 )
74 51 73 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = 1 )
75 elprob ⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ Prob ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = 1 ) )
76 49 74 75 sylanbrc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ Prob )