Metamath Proof Explorer

Theorem rrvmulc

Description: A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017) (Revised by Thierry Arnoux, 22-May-2017)

Ref Expression
Hypotheses rrvmulc.1 ⊢ φ → P ∈ Prob
rrvmulc.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
rrvmulc.3 ⊢ φ → C ∈ ℝ
Assertion rrvmulc ⊢ φ → X ∘ fc ⁡ × C ∈ RndVar ℝ ⁡ P

Proof

Step Hyp Ref Expression
1 rrvmulc.1 ⊢ φ → P ∈ Prob
2 rrvmulc.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
3 rrvmulc.3 ⊢ φ → C ∈ ℝ
4 1 2 rrvvf ⊢ φ → X : ⋃ dom ⁡ P ⟶ ℝ
5 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
6 1 5 syl ⊢ φ → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
7 6 uniexd ⊢ φ → ⋃ dom ⁡ P ∈ V
8 4 7 3 ofcfval4 ⊢ φ → X ∘ fc ⁡ × C = x ∈ ℝ ⟼ x ⁢ C ∘ X
9 brsigarn ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ
10 elrnsiga ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
11 9 10 mp1i ⊢ φ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
12 1 rrvmbfm ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
13 2 12 mpbid ⊢ φ → X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
14 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
15 14 3 rmulccn ⊢ φ → x ∈ ℝ ⟼ x ⁢ C ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ .
16 df-brsiga ⊢ 𝔅 ℝ = 𝛔 ⁡ topGen ⁡ ran ⁡ .
17 16 a1i ⊢ φ → 𝔅 ℝ = 𝛔 ⁡ topGen ⁡ ran ⁡ .
18 15 17 17 cnmbfm ⊢ φ → x ∈ ℝ ⟼ x ⁢ C ∈ 𝔅 ℝ MblFn μ 𝔅 ℝ
19 6 11 11 13 18 mbfmco ⊢ φ → x ∈ ℝ ⟼ x ⁢ C ∘ X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
20 8 19 eqeltrd ⊢ φ → X ∘ fc ⁡ × C ∈ dom ⁡ P MblFn μ 𝔅 ℝ
21 1 rrvmbfm ⊢ φ → X ∘ fc ⁡ × C ∈ RndVar ℝ ⁡ P ↔ X ∘ fc ⁡ × C ∈ dom ⁡ P MblFn μ 𝔅 ℝ
22 20 21 mpbird ⊢ φ → X ∘ fc ⁡ × C ∈ RndVar ℝ ⁡ P