Metamath Proof Explorer

Theorem totprobd

Description: Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Hypotheses totprobd.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
totprobd.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑃 )
totprobd.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 dom 𝑃 )
totprobd.4 ⊢ ( 𝜑 → ∪ 𝐵 = ∪ dom 𝑃 )
totprobd.5 ⊢ ( 𝜑 → 𝐵 ≼ ω )
totprobd.6 ⊢ ( 𝜑 → Disj 𝑏 ∈ 𝐵 𝑏 )
Assertion totprobd ( 𝜑 → ( 𝑃 ‘ 𝐴 ) = Σ* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 totprobd.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 totprobd.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑃 )
3 totprobd.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 dom 𝑃 )
4 totprobd.4 ⊢ ( 𝜑 → ∪ 𝐵 = ∪ dom 𝑃 )
5 totprobd.5 ⊢ ( 𝜑 → 𝐵 ≼ ω )
6 totprobd.6 ⊢ ( 𝜑 → Disj 𝑏 ∈ 𝐵 𝑏 )
7 elssuni ⊢ ( 𝐴 ∈ dom 𝑃 → 𝐴 ⊆ ∪ dom 𝑃 )
8 2 7 syl ⊢ ( 𝜑 → 𝐴 ⊆ ∪ dom 𝑃 )
9 8 4 sseqtrrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐵 )
10 sseqin2 ⊢ ( 𝐴 ⊆ ∪ 𝐵 ↔ ( ∪ 𝐵 ∩ 𝐴 ) = 𝐴 )
11 9 10 sylib ⊢ ( 𝜑 → ( ∪ 𝐵 ∩ 𝐴 ) = 𝐴 )
12 11 fveq2d ⊢ ( 𝜑 → ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) = ( 𝑃 ‘ 𝐴 ) )
13 domprobmeas ⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
14 1 13 syl ⊢ ( 𝜑 → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
15 measinb ⊢ ( ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ∈ ( measures ‘ dom 𝑃 ) )
16 14 2 15 syl2anc ⊢ ( 𝜑 → ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ∈ ( measures ‘ dom 𝑃 ) )
17 measvun ⊢ ( ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ∈ ( measures ‘ dom 𝑃 ) ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) → ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ ∪ 𝐵 ) = Σ* 𝑏 ∈ 𝐵 ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ 𝑏 ) )
18 16 3 5 6 17 syl112anc ⊢ ( 𝜑 → ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ ∪ 𝐵 ) = Σ* 𝑏 ∈ 𝐵 ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ 𝑏 ) )
19 eqidd ⊢ ( 𝜑 → ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) = ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑐 = ∪ 𝐵 ) → 𝑐 = ∪ 𝐵 )
21 20 ineq1d ⊢ ( ( 𝜑 ∧ 𝑐 = ∪ 𝐵 ) → ( 𝑐 ∩ 𝐴 ) = ( ∪ 𝐵 ∩ 𝐴 ) )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 = ∪ 𝐵 ) → ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) = ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) )
23 domprobsiga ⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
24 1 23 syl ⊢ ( 𝜑 → dom 𝑃 ∈ ∪ ran sigAlgebra )
25 sigaclcu ⊢ ( ( dom 𝑃 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ 𝐵 ≼ ω ) → ∪ 𝐵 ∈ dom 𝑃 )
26 24 3 5 25 syl3anc ⊢ ( 𝜑 → ∪ 𝐵 ∈ dom 𝑃 )
27 inelsiga ⊢ ( ( dom 𝑃 ∈ ∪ ran sigAlgebra ∧ ∪ 𝐵 ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) → ( ∪ 𝐵 ∩ 𝐴 ) ∈ dom 𝑃 )
28 24 26 2 27 syl3anc ⊢ ( 𝜑 → ( ∪ 𝐵 ∩ 𝐴 ) ∈ dom 𝑃 )
29 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ ( ∪ 𝐵 ∩ 𝐴 ) ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) ∈ ( 0 [,] 1 ) )
30 1 28 29 syl2anc ⊢ ( 𝜑 → ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) ∈ ( 0 [,] 1 ) )
31 19 22 26 30 fvmptd ⊢ ( 𝜑 → ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ ∪ 𝐵 ) = ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) )
32 eqidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) = ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 = 𝑏 ) → 𝑐 = 𝑏 )
34 33 ineq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 = 𝑏 ) → ( 𝑐 ∩ 𝐴 ) = ( 𝑏 ∩ 𝐴 ) )
35 34 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 = 𝑏 ) → ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) = ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
37 3 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ∈ 𝒫 dom 𝑃 )
38 elelpwi ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ) → 𝑏 ∈ dom 𝑃 )
39 36 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ dom 𝑃 )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑃 ∈ Prob )
41 24 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → dom 𝑃 ∈ ∪ ran sigAlgebra )
42 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ dom 𝑃 )
43 inelsiga ⊢ ( ( dom 𝑃 ∈ ∪ ran sigAlgebra ∧ 𝑏 ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑏 ∩ 𝐴 ) ∈ dom 𝑃 )
44 41 39 42 43 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ∩ 𝐴 ) ∈ dom 𝑃 )
45 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝑏 ∩ 𝐴 ) ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) ∈ ( 0 [,] 1 ) )
46 40 44 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) ∈ ( 0 [,] 1 ) )
47 32 35 39 46 fvmptd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ 𝑏 ) = ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )
48 47 esumeq2dv ⊢ ( 𝜑 → Σ* 𝑏 ∈ 𝐵 ( ( 𝑐 ∈ dom 𝑃 ↦ ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) ) ‘ 𝑏 ) = Σ* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )
49 18 31 48 3eqtr3d ⊢ ( 𝜑 → ( 𝑃 ‘ ( ∪ 𝐵 ∩ 𝐴 ) ) = Σ* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )
50 12 49 eqtr3d ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) = Σ* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )