Step | Hyp | Ref
| Expression |
1 | | dstrvprob.3 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦
(𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) |
2 | | dstrvprob.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ Prob) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
𝑃 ∈
Prob) |
4 | | dstrvprob.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) |
5 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
𝑋 ∈
(rRndVar‘𝑃)) |
6 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
𝑎 ∈
𝔅ℝ) |
7 | 3, 5, 6 | orvcelel 30531 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
(𝑋∘RV/𝑐 E 𝑎) ∈ dom 𝑃) |
8 | | prob01 30475 |
. . . . . . . 8
⊢ ((𝑃 ∈ Prob ∧ (𝑋∘RV/𝑐 E
𝑎) ∈ dom 𝑃) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
(0[,]1)) |
9 | 3, 7, 8 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
(𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
(0[,]1)) |
10 | | elunitrn 29943 |
. . . . . . . . 9
⊢ ((𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]1) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
ℝ) |
11 | 10 | rexrd 10089 |
. . . . . . . 8
⊢ ((𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]1) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
ℝ*) |
12 | | elunitge0 29945 |
. . . . . . . 8
⊢ ((𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]1) → 0 ≤
(𝑃‘(𝑋∘RV/𝑐 E 𝑎))) |
13 | | elxrge0 12281 |
. . . . . . . 8
⊢ ((𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]+∞) ↔
((𝑃‘(𝑋∘RV/𝑐 E
𝑎)) ∈
ℝ* ∧ 0 ≤ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) |
14 | 11, 12, 13 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]1) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
(0[,]+∞)) |
15 | 9, 14 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
(𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
(0[,]+∞)) |
16 | 1, 15 | fmpt3d 6386 |
. . . . 5
⊢ (𝜑 → 𝐷:𝔅ℝ⟶(0[,]+∞)) |
17 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 = ∅) → 𝑎 = ∅) |
18 | 17 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 = ∅) → (𝑋∘RV/𝑐 E 𝑎) = (𝑋∘RV/𝑐 E
∅)) |
19 | 18 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 = ∅) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) = (𝑃‘(𝑋∘RV/𝑐 E
∅))) |
20 | | brsigarn 30247 |
. . . . . . . . 9
⊢
𝔅ℝ ∈
(sigAlgebra‘ℝ) |
21 | | elrnsiga 30189 |
. . . . . . . . 9
⊢
(𝔅ℝ ∈ (sigAlgebra‘ℝ) →
𝔅ℝ ∈ ∪ ran
sigAlgebra) |
22 | | 0elsiga 30177 |
. . . . . . . . 9
⊢
(𝔅ℝ ∈ ∪ ran
sigAlgebra → ∅ ∈ 𝔅ℝ) |
23 | 20, 21, 22 | mp2b 10 |
. . . . . . . 8
⊢ ∅
∈ 𝔅ℝ |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ∅ ∈
𝔅ℝ) |
25 | 2, 4, 24 | orvcelel 30531 |
. . . . . . . 8
⊢ (𝜑 → (𝑋∘RV/𝑐 E ∅)
∈ dom 𝑃) |
26 | 2, 25 | probvalrnd 30486 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘(𝑋∘RV/𝑐 E ∅))
∈ ℝ) |
27 | 1, 19, 24, 26 | fvmptd 6288 |
. . . . . 6
⊢ (𝜑 → (𝐷‘∅) = (𝑃‘(𝑋∘RV/𝑐 E
∅))) |
28 | 2, 4, 24 | orvcelval 30530 |
. . . . . . 7
⊢ (𝜑 → (𝑋∘RV/𝑐 E ∅) =
(◡𝑋 “ ∅)) |
29 | 28 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (𝑃‘(𝑋∘RV/𝑐 E ∅)) =
(𝑃‘(◡𝑋 “ ∅))) |
30 | | ima0 5481 |
. . . . . . . 8
⊢ (◡𝑋 “ ∅) = ∅ |
31 | 30 | fveq2i 6194 |
. . . . . . 7
⊢ (𝑃‘(◡𝑋 “ ∅)) = (𝑃‘∅) |
32 | | probnul 30476 |
. . . . . . . 8
⊢ (𝑃 ∈ Prob → (𝑃‘∅) =
0) |
33 | 2, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘∅) = 0) |
34 | 31, 33 | syl5eq 2668 |
. . . . . 6
⊢ (𝜑 → (𝑃‘(◡𝑋 “ ∅)) = 0) |
35 | 27, 29, 34 | 3eqtrd 2660 |
. . . . 5
⊢ (𝜑 → (𝐷‘∅) = 0) |
36 | 2, 4 | rrvvf 30506 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ) |
37 | 36 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑋:∪ dom 𝑃⟶ℝ) |
38 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝑋:∪
dom 𝑃⟶ℝ →
Fun 𝑋) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → Fun 𝑋) |
40 | | unipreima 29446 |
. . . . . . . . . . 11
⊢ (Fun
𝑋 → (◡𝑋 “ ∪ 𝑥) = ∪ 𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎)) |
41 | 40 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (Fun
𝑋 → (𝑃‘(◡𝑋 “ ∪ 𝑥)) = (𝑃‘∪
𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎))) |
42 | 39, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝑃‘(◡𝑋 “ ∪ 𝑥)) = (𝑃‘∪
𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎))) |
43 | 2 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑃 ∈ Prob) |
44 | | domprobmeas 30472 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom
𝑃)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑃 ∈ (measures‘dom 𝑃)) |
46 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) |
47 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎 𝑥 ≼
ω |
48 | | nfdisj1 4633 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎Disj
𝑎 ∈ 𝑥 𝑎 |
49 | 47, 48 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(𝑥 ≼ ω ∧
Disj 𝑎 ∈ 𝑥 𝑎) |
50 | 46, 49 | nfan 1828 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) |
51 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝜑) |
52 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝑎 ∈ 𝑥) |
53 | | simpllr 799 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝑥 ∈ 𝒫
𝔅ℝ) |
54 | | elelpwi 4171 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) → 𝑎 ∈
𝔅ℝ) |
55 | 52, 53, 54 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝑎 ∈
𝔅ℝ) |
56 | 2, 4 | rrvfinvima 30512 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑎 ∈ 𝔅ℝ (◡𝑋 “ 𝑎) ∈ dom 𝑃) |
57 | 56 | r19.21bi 2932 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
(◡𝑋 “ 𝑎) ∈ dom 𝑃) |
58 | 51, 55, 57 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → (◡𝑋 “ 𝑎) ∈ dom 𝑃) |
59 | 58 | ex 450 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝑎 ∈ 𝑥 → (◡𝑋 “ 𝑎) ∈ dom 𝑃)) |
60 | 50, 59 | ralrimi 2957 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → ∀𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎) ∈ dom 𝑃) |
61 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑥 ≼ ω) |
62 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → Disj 𝑎 ∈ 𝑥 𝑎) |
63 | | disjpreima 29397 |
. . . . . . . . . . 11
⊢ ((Fun
𝑋 ∧ Disj 𝑎 ∈ 𝑥 𝑎) → Disj 𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎)) |
64 | 39, 62, 63 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → Disj 𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎)) |
65 | | measvuni 30277 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (measures‘dom
𝑃) ∧ ∀𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎) ∈ dom 𝑃 ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎))) → (𝑃‘∪
𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎)) = Σ*𝑎 ∈ 𝑥(𝑃‘(◡𝑋 “ 𝑎))) |
66 | 45, 60, 61, 64, 65 | syl112anc 1330 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝑃‘∪
𝑎 ∈ 𝑥 (◡𝑋 “ 𝑎)) = Σ*𝑎 ∈ 𝑥(𝑃‘(◡𝑋 “ 𝑎))) |
67 | 42, 66 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝑃‘(◡𝑋 “ ∪ 𝑥)) = Σ*𝑎 ∈ 𝑥(𝑃‘(◡𝑋 “ 𝑎))) |
68 | 4 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑋 ∈ (rRndVar‘𝑃)) |
69 | 1 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦
(𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) |
70 | 20, 21 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝔅ℝ ∈
∪ ran sigAlgebra) |
71 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → 𝑥 ∈ 𝒫
𝔅ℝ) |
72 | | sigaclcu 30180 |
. . . . . . . . . 10
⊢
((𝔅ℝ ∈ ∪ ran
sigAlgebra ∧ 𝑥 ∈
𝒫 𝔅ℝ ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝔅ℝ) |
73 | 70, 71, 61, 72 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → ∪ 𝑥 ∈
𝔅ℝ) |
74 | 43, 68, 69, 73 | dstrvval 30532 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝐷‘∪ 𝑥) = (𝑃‘(◡𝑋 “ ∪ 𝑥))) |
75 | 1, 9 | fvmpt2d 6293 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝔅ℝ) →
(𝐷‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 E 𝑎))) |
76 | 51, 55, 75 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → (𝐷‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 E 𝑎))) |
77 | 43 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝑃 ∈ Prob) |
78 | 68 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → 𝑋 ∈ (rRndVar‘𝑃)) |
79 | 77, 78, 55 | orvcelval 30530 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → (𝑋∘RV/𝑐 E 𝑎) = (◡𝑋 “ 𝑎)) |
80 | 79 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) = (𝑃‘(◡𝑋 “ 𝑎))) |
81 | 76, 80 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) ∧ 𝑎 ∈ 𝑥) → (𝐷‘𝑎) = (𝑃‘(◡𝑋 “ 𝑎))) |
82 | 81 | ex 450 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝑎 ∈ 𝑥 → (𝐷‘𝑎) = (𝑃‘(◡𝑋 “ 𝑎)))) |
83 | 50, 82 | ralrimi 2957 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → ∀𝑎 ∈ 𝑥 (𝐷‘𝑎) = (𝑃‘(◡𝑋 “ 𝑎))) |
84 | 50, 83 | esumeq2d 30099 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → Σ*𝑎 ∈ 𝑥(𝐷‘𝑎) = Σ*𝑎 ∈ 𝑥(𝑃‘(◡𝑋 “ 𝑎))) |
85 | 67, 74, 84 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) ∧ (𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎)) → (𝐷‘∪ 𝑥) = Σ*𝑎 ∈ 𝑥(𝐷‘𝑎)) |
86 | 85 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫
𝔅ℝ) → ((𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎) → (𝐷‘∪ 𝑥) = Σ*𝑎 ∈ 𝑥(𝐷‘𝑎))) |
87 | 86 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝒫
𝔅ℝ((𝑥 ≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎) → (𝐷‘∪ 𝑥) = Σ*𝑎 ∈ 𝑥(𝐷‘𝑎))) |
88 | | ismeas 30262 |
. . . . . 6
⊢
(𝔅ℝ ∈ ∪ ran
sigAlgebra → (𝐷 ∈
(measures‘𝔅ℝ) ↔ (𝐷:𝔅ℝ⟶(0[,]+∞)
∧ (𝐷‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝔅ℝ((𝑥
≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎) → (𝐷‘∪ 𝑥) = Σ*𝑎 ∈ 𝑥(𝐷‘𝑎))))) |
89 | 20, 21, 88 | mp2b 10 |
. . . . 5
⊢ (𝐷 ∈
(measures‘𝔅ℝ) ↔ (𝐷:𝔅ℝ⟶(0[,]+∞)
∧ (𝐷‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝔅ℝ((𝑥
≼ ω ∧ Disj 𝑎 ∈ 𝑥 𝑎) → (𝐷‘∪ 𝑥) = Σ*𝑎 ∈ 𝑥(𝐷‘𝑎)))) |
90 | 16, 35, 87, 89 | syl3anbrc 1246 |
. . . 4
⊢ (𝜑 → 𝐷 ∈
(measures‘𝔅ℝ)) |
91 | 1 | dmeqd 5326 |
. . . . . 6
⊢ (𝜑 → dom 𝐷 = dom (𝑎 ∈ 𝔅ℝ ↦
(𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) |
92 | 15 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ 𝔅ℝ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈
(0[,]+∞)) |
93 | | dmmptg 5632 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝔅ℝ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) ∈ (0[,]+∞) →
dom (𝑎 ∈
𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎))) =
𝔅ℝ) |
94 | 92, 93 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝑎 ∈ 𝔅ℝ ↦
(𝑃‘(𝑋∘RV/𝑐 E 𝑎))) =
𝔅ℝ) |
95 | 91, 94 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → dom 𝐷 =
𝔅ℝ) |
96 | 95 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (measures‘dom 𝐷) =
(measures‘𝔅ℝ)) |
97 | 90, 96 | eleqtrrd 2704 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (measures‘dom 𝐷)) |
98 | | measbasedom 30265 |
. . 3
⊢ (𝐷 ∈ ∪ ran measures ↔ 𝐷 ∈ (measures‘dom 𝐷)) |
99 | 97, 98 | sylibr 224 |
. 2
⊢ (𝜑 → 𝐷 ∈ ∪ ran
measures) |
100 | 95 | unieqd 4446 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝐷 = ∪
𝔅ℝ) |
101 | | unibrsiga 30249 |
. . . . 5
⊢ ∪ 𝔅ℝ = ℝ |
102 | 100, 101 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → ∪ dom 𝐷 = ℝ) |
103 | 102 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝐷‘∪ dom
𝐷) = (𝐷‘ℝ)) |
104 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 = ℝ) → 𝑎 = ℝ) |
105 | 104 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑋∘RV/𝑐 E 𝑎) = (𝑋∘RV/𝑐 E
ℝ)) |
106 | | baselsiga 30178 |
. . . . . . . . . 10
⊢
(𝔅ℝ ∈ (sigAlgebra‘ℝ) →
ℝ ∈ 𝔅ℝ) |
107 | 20, 106 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
𝔅ℝ) |
108 | 2, 4, 107 | orvcelval 30530 |
. . . . . . . 8
⊢ (𝜑 → (𝑋∘RV/𝑐 E ℝ) =
(◡𝑋 “ ℝ)) |
109 | 108 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑋∘RV/𝑐 E ℝ) =
(◡𝑋 “ ℝ)) |
110 | 105, 109 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑋∘RV/𝑐 E 𝑎) = (◡𝑋 “ ℝ)) |
111 | 110 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) = (𝑃‘(◡𝑋 “ ℝ))) |
112 | | fimacnv 6347 |
. . . . . . . . 9
⊢ (𝑋:∪
dom 𝑃⟶ℝ →
(◡𝑋 “ ℝ) = ∪ dom 𝑃) |
113 | 36, 112 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑋 “ ℝ) = ∪ dom 𝑃) |
114 | 113 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘(◡𝑋 “ ℝ)) = (𝑃‘∪ dom
𝑃)) |
115 | | probtot 30474 |
. . . . . . . 8
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) |
116 | 2, 115 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘∪ dom
𝑃) = 1) |
117 | 114, 116 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → (𝑃‘(◡𝑋 “ ℝ)) = 1) |
118 | 117 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑃‘(◡𝑋 “ ℝ)) = 1) |
119 | 111, 118 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 = ℝ) → (𝑃‘(𝑋∘RV/𝑐 E 𝑎)) = 1) |
120 | | 1red 10055 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
121 | 1, 119, 107, 120 | fvmptd 6288 |
. . 3
⊢ (𝜑 → (𝐷‘ℝ) = 1) |
122 | 103, 121 | eqtrd 2656 |
. 2
⊢ (𝜑 → (𝐷‘∪ dom
𝐷) = 1) |
123 | | elprob 30471 |
. 2
⊢ (𝐷 ∈ Prob ↔ (𝐷 ∈ ∪ ran measures ∧ (𝐷‘∪ dom
𝐷) = 1)) |
124 | 99, 122, 123 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐷 ∈ Prob) |