dstrvprob

Description: The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval ). (Contributed by Thierry Arnoux, 10-Feb-2017)

	Ref	Expression
Hypotheses	dstrvprob.1	$⊢ φ \to P \in Prob$
	dstrvprob.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
	dstrvprob.3	$⊢ φ \to D = (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a))$
Assertion	dstrvprob	$⊢ φ \to D \in Prob$

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	$⊢ φ \to P \in Prob$
2		dstrvprob.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		dstrvprob.3	$⊢ φ \to D = (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a))$
4	1	adantr	$⊢ (φ \land a \in 𝔅_{ℝ}) \to P \in Prob$
5	2	adantr	$⊢ (φ \land a \in 𝔅_{ℝ}) \to X \in {RndVar}_{ℝ} (P)$
6		simpr	$⊢ (φ \land a \in 𝔅_{ℝ}) \to a \in 𝔅_{ℝ}$
7	4 5 6	orvcelel	$⊢ (φ \land a \in 𝔅_{ℝ}) \to X E_{RV/c} a \in dom P$
8		prob01	$⊢ (P \in Prob \land X E_{RV/c} a \in dom P) \to P (X E_{RV/c} a) \in [0, 1]$
9	4 7 8	syl2anc	$⊢ (φ \land a \in 𝔅_{ℝ}) \to P (X E_{RV/c} a) \in [0, 1]$
10		elunitrn	$⊢ P (X E_{RV/c} a) \in [0, 1] \to P (X E_{RV/c} a) \in ℝ$
11	10	rexrd	$⊢ P (X E_{RV/c} a) \in [0, 1] \to P (X E_{RV/c} a) \in ℝ^{*}$
12		elunitge0	$⊢ P (X E_{RV/c} a) \in [0, 1] \to 0 \leq P (X E_{RV/c} a)$
13		elxrge0	$⊢ P (X E_{RV/c} a) \in [0, +∞] \leftrightarrow (P (X E_{RV/c} a) \in ℝ^{*} \land 0 \leq P (X E_{RV/c} a))$
14	11 12 13	sylanbrc	$⊢ P (X E_{RV/c} a) \in [0, 1] \to P (X E_{RV/c} a) \in [0, +∞]$
15	9 14	syl	$⊢ (φ \land a \in 𝔅_{ℝ}) \to P (X E_{RV/c} a) \in [0, +∞]$
16	3 15	fmpt3d	$⊢ φ \to D : 𝔅_{ℝ} ⟶ [0, +∞]$
17		simpr	$⊢ (φ \land a = \emptyset) \to a = \emptyset$
18	17	oveq2d	$⊢ (φ \land a = \emptyset) \to X E_{RV/c} a = X E_{RV/c} \emptyset$
19	18	fveq2d	$⊢ (φ \land a = \emptyset) \to P (X E_{RV/c} a) = P (X E_{RV/c} \emptyset)$
20		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
21		elrnsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
22		0elsiga	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra \to \emptyset \in 𝔅_{ℝ}$
23	20 21 22	mp2b	$⊢ \emptyset \in 𝔅_{ℝ}$
24	23	a1i	$⊢ φ \to \emptyset \in 𝔅_{ℝ}$
25	1 2 24	orvcelel	$⊢ φ \to X E_{RV/c} \emptyset \in dom P$
26	1 25	probvalrnd	$⊢ φ \to P (X E_{RV/c} \emptyset) \in ℝ$
27	3 19 24 26	fvmptd	$⊢ φ \to D (\emptyset) = P (X E_{RV/c} \emptyset)$
28	1 2 24	orvcelval	$⊢ φ \to X E_{RV/c} \emptyset = X^{-1} [\emptyset]$
29	28	fveq2d	$⊢ φ \to P (X E_{RV/c} \emptyset) = P (X^{-1} [\emptyset])$
30		ima0	$⊢ X^{-1} [\emptyset] = \emptyset$
31	30	fveq2i	$⊢ P (X^{-1} [\emptyset]) = P (\emptyset)$
32		probnul	$⊢ P \in Prob \to P (\emptyset) = 0$
33	1 32	syl	$⊢ φ \to P (\emptyset) = 0$
34	31 33	syl5eq	$⊢ φ \to P (X^{-1} [\emptyset]) = 0$
35	27 29 34	3eqtrd	$⊢ φ \to D (\emptyset) = 0$
36	1 2	rrvvf	$⊢ φ \to X : ⋃ dom P ⟶ ℝ$
37	36	ad2antrr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to X : ⋃ dom P ⟶ ℝ$
38	37	ffund	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to Fun X$
39		unipreima	$⊢ Fun X \to X^{-1} [⋃ x] = ⋃_{a \in x} X^{-1} [a]$
40	39	fveq2d	$⊢ Fun X \to P (X^{-1} [⋃ x]) = P (⋃_{a \in x} X^{-1} [a])$
41	38 40	syl	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to P (X^{-1} [⋃ x]) = P (⋃_{a \in x} X^{-1} [a])$
42	1	ad2antrr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to P \in Prob$
43		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
44	42 43	syl	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to P \in measures (dom P)$
45		nfv	$⊢ Ⅎ a (φ \land x \in 𝒫 𝔅_{ℝ})$
46		nfv	$⊢ Ⅎ a x ≼ ω$
47		nfdisj1	$⊢ Ⅎ a \underset{a \in x}{Disj} a$
48	46 47	nfan	$⊢ Ⅎ a (x ≼ ω \land \underset{a \in x}{Disj} a)$
49	45 48	nfan	$⊢ Ⅎ a ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a))$
50		simplll	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to φ$
51		simpr	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to a \in x$
52		simpllr	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to x \in 𝒫 𝔅_{ℝ}$
53		elelpwi	$⊢ (a \in x \land x \in 𝒫 𝔅_{ℝ}) \to a \in 𝔅_{ℝ}$
54	51 52 53	syl2anc	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to a \in 𝔅_{ℝ}$
55	1 2	rrvfinvima	$⊢ φ \to \forall a \in 𝔅_{ℝ} X^{-1} [a] \in dom P$
56	55	r19.21bi	$⊢ (φ \land a \in 𝔅_{ℝ}) \to X^{-1} [a] \in dom P$
57	50 54 56	syl2anc	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to X^{-1} [a] \in dom P$
58	57	ex	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to (a \in x \to X^{-1} [a] \in dom P)$
59	49 58	ralrimi	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to \forall a \in x X^{-1} [a] \in dom P$
60		simprl	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to x ≼ ω$
61		simprr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to \underset{a \in x}{Disj} a$
62		disjpreima	$⊢ (Fun X \land \underset{a \in x}{Disj} a) \to \underset{a \in x}{Disj} X^{-1} [a]$
63	38 61 62	syl2anc	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to \underset{a \in x}{Disj} X^{-1} [a]$
64		measvuni	$⊢ (P \in measures (dom P) \land \forall a \in x X^{-1} [a] \in dom P \land (x ≼ ω \land \underset{a \in x}{Disj} X^{-1} [a])) \to P (⋃_{a \in x} X^{-1} [a]) = \underset{a \in x}{\sum^{*}} P (X^{-1} [a])$
65	44 59 60 63 64	syl112anc	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to P (⋃_{a \in x} X^{-1} [a]) = \underset{a \in x}{\sum^{*}} P (X^{-1} [a])$
66	41 65	eqtrd	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to P (X^{-1} [⋃ x]) = \underset{a \in x}{\sum^{*}} P (X^{-1} [a])$
67	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to X \in {RndVar}_{ℝ} (P)$
68	3	ad2antrr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to D = (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a))$
69	20 21	mp1i	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
70		simplr	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to x \in 𝒫 𝔅_{ℝ}$
71		sigaclcu	$⊢ (𝔅_{ℝ} \in ⋃ ran sigAlgebra \land x \in 𝒫 𝔅_{ℝ} \land x ≼ ω) \to ⋃ x \in 𝔅_{ℝ}$
72	69 70 60 71	syl3anc	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to ⋃ x \in 𝔅_{ℝ}$
73	42 67 68 72	dstrvval	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to D (⋃ x) = P (X^{-1} [⋃ x])$
74	3 9	fvmpt2d	$⊢ (φ \land a \in 𝔅_{ℝ}) \to D (a) = P (X E_{RV/c} a)$
75	50 54 74	syl2anc	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to D (a) = P (X E_{RV/c} a)$
76	42	adantr	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to P \in Prob$
77	67	adantr	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to X \in {RndVar}_{ℝ} (P)$
78	76 77 54	orvcelval	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to X E_{RV/c} a = X^{-1} [a]$
79	78	fveq2d	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to P (X E_{RV/c} a) = P (X^{-1} [a])$
80	75 79	eqtrd	$⊢ (((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \land a \in x) \to D (a) = P (X^{-1} [a])$
81	80	ex	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to (a \in x \to D (a) = P (X^{-1} [a]))$
82	49 81	ralrimi	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to \forall a \in x D (a) = P (X^{-1} [a])$
83	49 82	esumeq2d	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to \underset{a \in x}{\sum^{}} D (a) = \underset{a \in x}{\sum^{}} P (X^{-1} [a])$
84	66 73 83	3eqtr4d	$⊢ ((φ \land x \in 𝒫 𝔅_{ℝ}) \land (x ≼ ω \land \underset{a \in x}{Disj} a)) \to D (⋃ x) = \underset{a \in x}{\sum^{*}} D (a)$
85	84	ex	$⊢ (φ \land x \in 𝒫 𝔅_{ℝ}) \to ((x ≼ ω \land \underset{a \in x}{Disj} a) \to D (⋃ x) = \underset{a \in x}{\sum^{*}} D (a))$
86	85	ralrimiva	$⊢ φ \to \forall x \in 𝒫 𝔅_{ℝ} ((x ≼ ω \land \underset{a \in x}{Disj} a) \to D (⋃ x) = \underset{a \in x}{\sum^{*}} D (a))$
87		ismeas	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra \to (D \in measures (𝔅_{ℝ}) \leftrightarrow (D : 𝔅_{ℝ} ⟶ [0, +∞] \land D (\emptyset) = 0 \land \forall x \in 𝒫 𝔅_{ℝ} ((x ≼ ω \land \underset{a \in x}{Disj} a) \to D (⋃ x) = \underset{a \in x}{\sum^{*}} D (a))))$
88	20 21 87	mp2b	$⊢ D \in measures (𝔅_{ℝ}) \leftrightarrow (D : 𝔅_{ℝ} ⟶ [0, +∞] \land D (\emptyset) = 0 \land \forall x \in 𝒫 𝔅_{ℝ} ((x ≼ ω \land \underset{a \in x}{Disj} a) \to D (⋃ x) = \underset{a \in x}{\sum^{*}} D (a)))$
89	16 35 86 88	syl3anbrc	$⊢ φ \to D \in measures (𝔅_{ℝ})$
90	3	dmeqd	$⊢ φ \to dom D = dom (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a))$
91	15	ralrimiva	$⊢ φ \to \forall a \in 𝔅_{ℝ} P (X E_{RV/c} a) \in [0, +∞]$
92		dmmptg	$⊢ \forall a \in 𝔅_{ℝ} P (X E_{RV/c} a) \in [0, +∞] \to dom (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a)) = 𝔅_{ℝ}$
93	91 92	syl	$⊢ φ \to dom (a \in 𝔅_{ℝ} ⟼ P (X E_{RV/c} a)) = 𝔅_{ℝ}$
94	90 93	eqtrd	$⊢ φ \to dom D = 𝔅_{ℝ}$
95	94	fveq2d	$⊢ φ \to measures (dom D) = measures (𝔅_{ℝ})$
96	89 95	eleqtrrd	$⊢ φ \to D \in measures (dom D)$
97		measbasedom	$⊢ D \in ⋃ ran measures \leftrightarrow D \in measures (dom D)$
98	96 97	sylibr	$⊢ φ \to D \in ⋃ ran measures$
99	94	unieqd	$⊢ φ \to ⋃ dom D = ⋃ 𝔅_{ℝ}$
100		unibrsiga	$⊢ ⋃ 𝔅_{ℝ} = ℝ$
101	99 100	eqtrdi	$⊢ φ \to ⋃ dom D = ℝ$
102	101	fveq2d	$⊢ φ \to D (⋃ dom D) = D (ℝ)$
103		simpr	$⊢ (φ \land a = ℝ) \to a = ℝ$
104	103	oveq2d	$⊢ (φ \land a = ℝ) \to X E_{RV/c} a = X E_{RV/c} ℝ$
105		baselsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to ℝ \in 𝔅_{ℝ}$
106	20 105	mp1i	$⊢ φ \to ℝ \in 𝔅_{ℝ}$
107	1 2 106	orvcelval	$⊢ φ \to X E_{RV/c} ℝ = X^{-1} [ℝ]$
108	107	adantr	$⊢ (φ \land a = ℝ) \to X E_{RV/c} ℝ = X^{-1} [ℝ]$
109	104 108	eqtrd	$⊢ (φ \land a = ℝ) \to X E_{RV/c} a = X^{-1} [ℝ]$
110	109	fveq2d	$⊢ (φ \land a = ℝ) \to P (X E_{RV/c} a) = P (X^{-1} [ℝ])$
111		fimacnv	$⊢ X : ⋃ dom P ⟶ ℝ \to X^{-1} [ℝ] = ⋃ dom P$
112	36 111	syl	$⊢ φ \to X^{-1} [ℝ] = ⋃ dom P$
113	112	fveq2d	$⊢ φ \to P (X^{-1} [ℝ]) = P (⋃ dom P)$
114		probtot	$⊢ P \in Prob \to P (⋃ dom P) = 1$
115	1 114	syl	$⊢ φ \to P (⋃ dom P) = 1$
116	113 115	eqtrd	$⊢ φ \to P (X^{-1} [ℝ]) = 1$
117	116	adantr	$⊢ (φ \land a = ℝ) \to P (X^{-1} [ℝ]) = 1$
118	110 117	eqtrd	$⊢ (φ \land a = ℝ) \to P (X E_{RV/c} a) = 1$
119		1red	$⊢ φ \to 1 \in ℝ$
120	3 118 106 119	fvmptd	$⊢ φ \to D (ℝ) = 1$
121	102 120	eqtrd	$⊢ φ \to D (⋃ dom D) = 1$
122		elprob	$⊢ D \in Prob \leftrightarrow (D \in ⋃ ran measures \land D (⋃ dom D) = 1)$
123	98 121 122	sylanbrc	$⊢ φ \to D \in Prob$

Metamath Proof Explorer

Theorem dstrvprob

Proof