Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
dstrvprob.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
dstrvprob.3 ⊢ ( 𝜑 → 𝐷 = ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) )
Assertion dstrvprob ( 𝜑 → 𝐷 ∈ Prob )

Proof

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