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	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	rrvmulc.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	rrvmulc.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	rrvmulc	⊢ ( 𝜑 → ( 𝑋 ∘f/c · 𝐶 ) ∈ ( rRndVar ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		rrvmulc.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		rrvmulc.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		rrvmulc.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4	1 2	rrvvf	⊢ ( 𝜑 → 𝑋 : ∪ dom 𝑃 ⟶ ℝ )
5		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
6	1 5	syl	⊢ ( 𝜑 → dom 𝑃 ∈ ∪ ran sigAlgebra )
7	6	uniexd	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ V )
8	4 7 3	ofcfval4	⊢ ( 𝜑 → ( 𝑋 ∘f/c · 𝐶 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∘ 𝑋 ) )
9		brsigarn	⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
10		elrnsiga	⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
11	9 10	mp1i	⊢ ( 𝜑 → 𝔅ℝ ∈ ∪ ran sigAlgebra )
12	1	rrvmbfm	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
13	2 12	mpbid	⊢ ( 𝜑 → 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
14		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
15	14 3	rmulccn	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
16		df-brsiga	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
17	16	a1i	⊢ ( 𝜑 → 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
18	15 17 17	cnmbfm	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( 𝔅ℝ MblFnM 𝔅ℝ ) )
19	6 11 11 13 18	mbfmco	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∘ 𝑋 ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
20	8 19	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ∘f/c · 𝐶 ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
21	1	rrvmbfm	⊢ ( 𝜑 → ( ( 𝑋 ∘f/c · 𝐶 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 ∘f/c · 𝐶 ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
22	20 21	mpbird	⊢ ( 𝜑 → ( 𝑋 ∘f/c · 𝐶 ) ∈ ( rRndVar ‘ 𝑃 ) )