totprobd

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

	Ref	Expression
Hypotheses	totprobd.1	$⊢ φ \to P \in Prob$
	totprobd.2	$⊢ φ \to A \in dom P$
	totprobd.3	$⊢ φ \to B \in 𝒫 dom P$
	totprobd.4	$⊢ φ \to ⋃ B = ⋃ dom P$
	totprobd.5	$⊢ φ \to B ≼ ω$
	totprobd.6	$⊢ φ \to \underset{b \in B}{Disj} b$
Assertion	totprobd	$⊢ φ \to P (A) = \underset{b \in B}{\sum^{*}} P (b \cap A)$

Proof

Step	Hyp	Ref	Expression
1		totprobd.1	$⊢ φ \to P \in Prob$
2		totprobd.2	$⊢ φ \to A \in dom P$
3		totprobd.3	$⊢ φ \to B \in 𝒫 dom P$
4		totprobd.4	$⊢ φ \to ⋃ B = ⋃ dom P$
5		totprobd.5	$⊢ φ \to B ≼ ω$
6		totprobd.6	$⊢ φ \to \underset{b \in B}{Disj} b$
7		elssuni	$⊢ A \in dom P \to A \subseteq ⋃ dom P$
8	2 7	syl	$⊢ φ \to A \subseteq ⋃ dom P$
9	8 4	sseqtrrd	$⊢ φ \to A \subseteq ⋃ B$
10		sseqin2	$⊢ A \subseteq ⋃ B \leftrightarrow ⋃ B \cap A = A$
11	9 10	sylib	$⊢ φ \to ⋃ B \cap A = A$
12	11	fveq2d	$⊢ φ \to P (⋃ B \cap A) = P (A)$
13		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
14	1 13	syl	$⊢ φ \to P \in measures (dom P)$
15		measinb	$⊢ (P \in measures (dom P) \land A \in dom P) \to (c \in dom P ⟼ P (c \cap A)) \in measures (dom P)$
16	14 2 15	syl2anc	$⊢ φ \to (c \in dom P ⟼ P (c \cap A)) \in measures (dom P)$
17		measvun	$⊢ ((c \in dom P ⟼ P (c \cap A)) \in measures (dom P) \land B \in 𝒫 dom P \land (B ≼ ω \land \underset{b \in B}{Disj} b)) \to (c \in dom P ⟼ P (c \cap A)) (⋃ B) = \underset{b \in B}{\sum^{*}} (c \in dom P ⟼ P (c \cap A)) (b)$
18	16 3 5 6 17	syl112anc	$⊢ φ \to (c \in dom P ⟼ P (c \cap A)) (⋃ B) = \underset{b \in B}{\sum^{*}} (c \in dom P ⟼ P (c \cap A)) (b)$
19		eqidd	$⊢ φ \to (c \in dom P ⟼ P (c \cap A)) = (c \in dom P ⟼ P (c \cap A))$
20		simpr	$⊢ (φ \land c = ⋃ B) \to c = ⋃ B$
21	20	ineq1d	$⊢ (φ \land c = ⋃ B) \to c \cap A = ⋃ B \cap A$
22	21	fveq2d	$⊢ (φ \land c = ⋃ B) \to P (c \cap A) = P (⋃ B \cap A)$
23		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
24	1 23	syl	$⊢ φ \to dom P \in ⋃ ran sigAlgebra$
25		sigaclcu	$⊢ (dom P \in ⋃ ran sigAlgebra \land B \in 𝒫 dom P \land B ≼ ω) \to ⋃ B \in dom P$
26	24 3 5 25	syl3anc	$⊢ φ \to ⋃ B \in dom P$
27		inelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land ⋃ B \in dom P \land A \in dom P) \to ⋃ B \cap A \in dom P$
28	24 26 2 27	syl3anc	$⊢ φ \to ⋃ B \cap A \in dom P$
29		prob01	$⊢ (P \in Prob \land ⋃ B \cap A \in dom P) \to P (⋃ B \cap A) \in [0, 1]$
30	1 28 29	syl2anc	$⊢ φ \to P (⋃ B \cap A) \in [0, 1]$
31	19 22 26 30	fvmptd	$⊢ φ \to (c \in dom P ⟼ P (c \cap A)) (⋃ B) = P (⋃ B \cap A)$
32		eqidd	$⊢ (φ \land b \in B) \to (c \in dom P ⟼ P (c \cap A)) = (c \in dom P ⟼ P (c \cap A))$
33		simpr	$⊢ ((φ \land b \in B) \land c = b) \to c = b$
34	33	ineq1d	$⊢ ((φ \land b \in B) \land c = b) \to c \cap A = b \cap A$
35	34	fveq2d	$⊢ ((φ \land b \in B) \land c = b) \to P (c \cap A) = P (b \cap A)$
36		simpr	$⊢ (φ \land b \in B) \to b \in B$
37	3	adantr	$⊢ (φ \land b \in B) \to B \in 𝒫 dom P$
38		elelpwi	$⊢ (b \in B \land B \in 𝒫 dom P) \to b \in dom P$
39	36 37 38	syl2anc	$⊢ (φ \land b \in B) \to b \in dom P$
40	1	adantr	$⊢ (φ \land b \in B) \to P \in Prob$
41	24	adantr	$⊢ (φ \land b \in B) \to dom P \in ⋃ ran sigAlgebra$
42	2	adantr	$⊢ (φ \land b \in B) \to A \in dom P$
43		inelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land b \in dom P \land A \in dom P) \to b \cap A \in dom P$
44	41 39 42 43	syl3anc	$⊢ (φ \land b \in B) \to b \cap A \in dom P$
45		prob01	$⊢ (P \in Prob \land b \cap A \in dom P) \to P (b \cap A) \in [0, 1]$
46	40 44 45	syl2anc	$⊢ (φ \land b \in B) \to P (b \cap A) \in [0, 1]$
47	32 35 39 46	fvmptd	$⊢ (φ \land b \in B) \to (c \in dom P ⟼ P (c \cap A)) (b) = P (b \cap A)$
48	47	esumeq2dv	$⊢ φ \to \underset{b \in B}{\sum^{}} (c \in dom P ⟼ P (c \cap A)) (b) = \underset{b \in B}{\sum^{}} P (b \cap A)$
49	18 31 48	3eqtr3d	$⊢ φ \to P (⋃ B \cap A) = \underset{b \in B}{\sum^{*}} P (b \cap A)$
50	12 49	eqtr3d	$⊢ φ \to P (A) = \underset{b \in B}{\sum^{*}} P (b \cap A)$

Metamath Proof Explorer

Theorem totprobd

Proof