probfinmeasb

Description: Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017)

		Ref	Expression
	Assertion	probfinmeasb	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} M (⋃ S) \in Prob$

Proof

Step	Hyp	Ref	Expression
1		measdivcst	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} M (⋃ S) \in measures (S)$
2		measfn	$⊢ M \in measures (S) \to M Fn S$
3	2	adantr	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M Fn S$
4		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
5	4	adantr	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to S \in ⋃ ran sigAlgebra$
6		simpr	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M (⋃ S) \in ℝ^{+}$
7	3 5 6	ofcfn	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (M \circ_{fc} \div_{𝑒} M (⋃ S)) Fn S$
8	7	fndmd	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to dom (M \circ_{fc} \div_{𝑒} M (⋃ S)) = S$
9	8	fveq2d	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to measures (dom (M \circ_{fc} \div_{𝑒} M (⋃ S))) = measures (S)$
10	1 9	eleqtrrd	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} M (⋃ S) \in measures (dom (M \circ_{fc} \div_{𝑒} M (⋃ S)))$
11		measbasedom	$⊢ M \circ_{fc} \div_{𝑒} M (⋃ S) \in ⋃ ran measures \leftrightarrow M \circ_{fc} \div_{𝑒} M (⋃ S) \in measures (dom (M \circ_{fc} \div_{𝑒} M (⋃ S)))$
12	10 11	sylibr	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} M (⋃ S) \in ⋃ ran measures$
13	8	unieqd	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to ⋃ dom (M \circ_{fc} \div_{𝑒} M (⋃ S)) = ⋃ S$
14	13	fveq2d	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ dom (M \circ_{fc} \div_{𝑒} M (⋃ S))) = (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ S)$
15		unielsiga	$⊢ S \in ⋃ ran sigAlgebra \to ⋃ S \in S$
16	5 15	syl	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to ⋃ S \in S$
17		eqidd	$⊢ ((M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \land ⋃ S \in S) \to M (⋃ S) = M (⋃ S)$
18	3 5 6 17	ofcval	$⊢ ((M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \land ⋃ S \in S) \to (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ S) = M (⋃ S) \div_{𝑒} M (⋃ S)$
19	16 18	mpdan	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ S) = M (⋃ S) \div_{𝑒} M (⋃ S)$
20		rpre	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \in ℝ$
21		rpne0	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \neq 0$
22		xdivid	$⊢ (M (⋃ S) \in ℝ \land M (⋃ S) \neq 0) \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
23	20 21 22	syl2anc	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
24	23	adantl	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
25	14 19 24	3eqtrd	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ dom (M \circ_{fc} \div_{𝑒} M (⋃ S))) = 1$
26		elprob	$⊢ M \circ_{fc} \div_{𝑒} M (⋃ S) \in Prob \leftrightarrow (M \circ_{fc} \div_{𝑒} M (⋃ S) \in ⋃ ran measures \land (M \circ_{fc} \div_{𝑒} M (⋃ S)) (⋃ dom (M \circ_{fc} \div_{𝑒} M (⋃ S))) = 1)$
27	12 25 26	sylanbrc	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} M (⋃ S) \in Prob$

Metamath Proof Explorer

Theorem probfinmeasb

Proof