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	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in Prob$

Proof

Step	Hyp	Ref	Expression
1		measinb	$⊢ (M \in measures (S) \land A \in S) \to (y \in S ⟼ M (y \cap A)) \in measures (S)$
2		measdivcstALTV	$⊢ ((y \in S ⟼ M (y \cap A)) \in measures (S) \land M (A) \in ℝ^{+}) \to (x \in S ⟼ (y \in S ⟼ M (y \cap A)) (x) \div_{𝑒} M (A)) \in measures (S)$
3	1 2	stoic3	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ (y \in S ⟼ M (y \cap A)) (x) \div_{𝑒} M (A)) \in measures (S)$
4		eqidd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to (y \in S ⟼ M (y \cap A)) = (y \in S ⟼ M (y \cap A))$
5		simpr	$⊢ (((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \land y = x) \to y = x$
6	5	ineq1d	$⊢ (((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \land y = x) \to y \cap A = x \cap A$
7	6	fveq2d	$⊢ (((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \land y = x) \to M (y \cap A) = M (x \cap A)$
8		simpr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to x \in S$
9		simp1	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to M \in measures (S)$
10	9	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M \in measures (S)$
11		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
12	10 11	syl	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to S \in ⋃ ran sigAlgebra$
13		simp2	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to A \in S$
14	13	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to A \in S$
15		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land x \in S \land A \in S) \to x \cap A \in S$
16	12 8 14 15	syl3anc	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to x \cap A \in S$
17		measvxrge0	$⊢ (M \in measures (S) \land x \cap A \in S) \to M (x \cap A) \in [0, +∞]$
18	10 16 17	syl2anc	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (x \cap A) \in [0, +∞]$
19	4 7 8 18	fvmptd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to (y \in S ⟼ M (y \cap A)) (x) = M (x \cap A)$
20	19	oveq1d	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to (y \in S ⟼ M (y \cap A)) (x) \div_{𝑒} M (A) = M (x \cap A) \div_{𝑒} M (A)$
21		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
22	21 18	sselid	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (x \cap A) \in ℝ^{*}$
23		simp3	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to M (A) \in ℝ^{+}$
24	23	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (A) \in ℝ^{+}$
25	24	rpred	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (A) \in ℝ$
26		0xr	$⊢ 0 \in ℝ^{*}$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land M (x \cap A) \in [0, +∞]) \to 0 \leq M (x \cap A)$
29	26 27 28	mp3an12	$⊢ M (x \cap A) \in [0, +∞] \to 0 \leq M (x \cap A)$
30	18 29	syl	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to 0 \leq M (x \cap A)$
31		inss2	$⊢ x \cap A \subseteq A$
32	31	a1i	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to x \cap A \subseteq A$
33	10 16 14 32	measssd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (x \cap A) \leq M (A)$
34		xrrege0	$⊢ ((M (x \cap A) \in ℝ^{*} \land M (A) \in ℝ) \land (0 \leq M (x \cap A) \land M (x \cap A) \leq M (A))) \to M (x \cap A) \in ℝ$
35	22 25 30 33 34	syl22anc	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (x \cap A) \in ℝ$
36	24	rpne0d	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (A) \neq 0$
37		rexdiv	$⊢ (M (x \cap A) \in ℝ \land M (A) \in ℝ \land M (A) \neq 0) \to M (x \cap A) \div_{𝑒} M (A) = \frac{M (x \cap A)}{M (A)}$
38	35 25 36 37	syl3anc	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to M (x \cap A) \div_{𝑒} M (A) = \frac{M (x \cap A)}{M (A)}$
39	20 38	eqtrd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to (y \in S ⟼ M (y \cap A)) (x) \div_{𝑒} M (A) = \frac{M (x \cap A)}{M (A)}$
40	39	mpteq2dva	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ (y \in S ⟼ M (y \cap A)) (x) \div_{𝑒} M (A)) = (x \in S ⟼ \frac{M (x \cap A)}{M (A)})$
41	35 24	rerpdivcld	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x \in S) \to \frac{M (x \cap A)}{M (A)} \in ℝ$
42	41	ralrimiva	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to \forall x \in S \frac{M (x \cap A)}{M (A)} \in ℝ$
43		dmmptg	$⊢ \forall x \in S \frac{M (x \cap A)}{M (A)} \in ℝ \to dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) = S$
44	42 43	syl	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) = S$
45	44	fveq2d	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to measures (dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)})) = measures (S)$
46	45	eqcomd	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to measures (S) = measures (dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}))$
47	3 40 46	3eltr3d	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in measures (dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}))$
48		measbasedom	$⊢ (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in ⋃ ran measures \leftrightarrow (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in measures (dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}))$
49	47 48	sylibr	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in ⋃ ran measures$
50	44	unieqd	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to ⋃ dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) = ⋃ S$
51	50	fveq2d	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) (⋃ dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)})) = (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) (⋃ S)$
52		eqidd	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) = (x \in S ⟼ \frac{M (x \cap A)}{M (A)})$
53	23	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to M (A) \in ℝ^{+}$
54	53	rpcnd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to M (A) \in ℂ$
55	23	rpne0d	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to M (A) \neq 0$
56	55	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to M (A) \neq 0$
57		simpr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to x = ⋃ S$
58	57	ineq1d	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to x \cap A = ⋃ S \cap A$
59		incom	$⊢ ⋃ S \cap A = A \cap ⋃ S$
60		elssuni	$⊢ A \in S \to A \subseteq ⋃ S$
61		df-ss	$⊢ A \subseteq ⋃ S \leftrightarrow A \cap ⋃ S = A$
62	60 61	sylib	$⊢ A \in S \to A \cap ⋃ S = A$
63	59 62	eqtrid	$⊢ A \in S \to ⋃ S \cap A = A$
64	13 63	syl	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to ⋃ S \cap A = A$
65	64	adantr	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to ⋃ S \cap A = A$
66	58 65	eqtrd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to x \cap A = A$
67	66	fveq2d	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to M (x \cap A) = M (A)$
68	54 56 67	diveq1bd	$⊢ ((M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \land x = ⋃ S) \to \frac{M (x \cap A)}{M (A)} = 1$
69		sgon	$⊢ S \in ⋃ ran sigAlgebra \to S \in sigAlgebra (⋃ S)$
70		baselsiga	$⊢ S \in sigAlgebra (⋃ S) \to ⋃ S \in S$
71	9 11 69 70	4syl	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to ⋃ S \in S$
72		1red	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to 1 \in ℝ$
73	52 68 71 72	fvmptd	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) (⋃ S) = 1$
74	51 73	eqtrd	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) (⋃ dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)})) = 1$
75		elprob	$⊢ (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in Prob \leftrightarrow ((x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in ⋃ ran measures \land (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) (⋃ dom (x \in S ⟼ \frac{M (x \cap A)}{M (A)})) = 1)$
76	49 74 75	sylanbrc	$⊢ (M \in measures (S) \land A \in S \land M (A) \in ℝ^{+}) \to (x \in S ⟼ \frac{M (x \cap A)}{M (A)}) \in Prob$

Metamath Proof Explorer

Theorem probmeasb

Proof