probfinmeasbALTV

Description: Alternate version of probfinmeasb . (Contributed by Thierry Arnoux, 17-Dec-2016) (New usage is discouraged.)

		Ref	Expression
	Assertion	probfinmeasbALTV	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in Prob$

Proof

Step	Hyp	Ref	Expression
1		measdivcstALTV	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in measures (S)$
2		ovex	$⊢ M (x) \div_{𝑒} M (⋃ S) \in V$
3	2	rgenw	$⊢ \forall x \in S M (x) \div_{𝑒} M (⋃ S) \in V$
4		dmmptg	$⊢ \forall x \in S M (x) \div_{𝑒} M (⋃ S) \in V \to dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) = S$
5	3 4	ax-mp	$⊢ dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) = S$
6	5	fveq2i	$⊢ measures (dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S))) = measures (S)$
7	1 6	eleqtrrdi	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in measures (dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)))$
8		measbasedom	$⊢ (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in ⋃ ran measures \leftrightarrow (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in measures (dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)))$
9	7 8	sylibr	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in ⋃ ran measures$
10	5	unieqi	$⊢ ⋃ dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) = ⋃ S$
11	10	fveq2i	$⊢ (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S))) = (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ S)$
12		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
13		isrnsigau	$⊢ S \in ⋃ ran sigAlgebra \to (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)))$
14	13	simprd	$⊢ S \in ⋃ ran sigAlgebra \to (⋃ S \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S))$
15	14	simp1d	$⊢ S \in ⋃ ran sigAlgebra \to ⋃ S \in S$
16	12 15	syl	$⊢ M \in measures (S) \to ⋃ S \in S$
17		id	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \in ℝ^{+}$
18	17 17	rpxdivcld	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \div_{𝑒} M (⋃ S) \in ℝ^{+}$
19	16 18	anim12i	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (⋃ S \in S \land M (⋃ S) \div_{𝑒} M (⋃ S) \in ℝ^{+})$
20		fveq2	$⊢ x = ⋃ S \to M (x) = M (⋃ S)$
21	20	oveq1d	$⊢ x = ⋃ S \to M (x) \div_{𝑒} M (⋃ S) = M (⋃ S) \div_{𝑒} M (⋃ S)$
22		eqid	$⊢ (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) = (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S))$
23	21 22	fvmptg	$⊢ (⋃ S \in S \land M (⋃ S) \div_{𝑒} M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ S) = M (⋃ S) \div_{𝑒} M (⋃ S)$
24	19 23	syl	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ S) = M (⋃ S) \div_{𝑒} M (⋃ S)$
25		rpre	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \in ℝ$
26		rpne0	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \neq 0$
27		xdivid	$⊢ (M (⋃ S) \in ℝ \land M (⋃ S) \neq 0) \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
28	25 26 27	syl2anc	$⊢ M (⋃ S) \in ℝ^{+} \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
29	28	adantl	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to M (⋃ S) \div_{𝑒} M (⋃ S) = 1$
30	24 29	eqtrd	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ S) = 1$
31	11 30	eqtrid	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S))) = 1$
32		elprob	$⊢ (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in Prob \leftrightarrow ((x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in ⋃ ran measures \land (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) (⋃ dom (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S))) = 1)$
33	9 31 32	sylanbrc	$⊢ (M \in measures (S) \land M (⋃ S) \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} M (⋃ S)) \in Prob$

Metamath Proof Explorer

Theorem probfinmeasbALTV

Proof