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	$$⊢\phi \to P\in \mathrm{Prob}$$
	rrvmulc.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	rrvmulc.3	$$⊢\phi \to C\in ℝ$$
Assertion	rrvmulc	$$⊢\phi \to X{\circ }_{\mathrm{fc}}\times C\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrvmulc.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		rrvmulc.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3		rrvmulc.3	$$⊢\phi \to C\in ℝ$$
4	1 2	rrvvf	$$⊢\phi \to X:\bigcup \mathrm{dom}P⟶ℝ$$
5		domprobsiga	$$⊢P\in \mathrm{Prob}\to \mathrm{dom}P\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
6	1 5	syl	$$⊢\phi \to \mathrm{dom}P\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
7	6	uniexd	$$⊢\phi \to \bigcup \mathrm{dom}P\in \mathrm{V}$$
8	4 7 3	ofcfval4	$$⊢\phi \to X{\circ }_{\mathrm{fc}}\times C=\left(x\in ℝ⟼xC\right)\circ X$$
9		brsigarn	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$$
10		elrnsiga	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)\to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
11	9 10	mp1i	$$⊢\phi \to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
12	1	rrvmbfm	$$⊢\phi \to \left(X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$
13	2 12	mpbid	$$⊢\phi \to X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
14		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
15	14 3	rmulccn	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
16		df-brsiga	$$⊢{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
17	16	a1i	$$⊢\phi \to {𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
18	15 17 17	cnmbfm	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\in \left({𝔅}_{ℝ}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
19	6 11 11 13 18	mbfmco	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\circ X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
20	8 19	eqeltrd	$$⊢\phi \to X{\circ }_{\mathrm{fc}}\times C\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
21	1	rrvmbfm	$$⊢\phi \to \left(X{\circ }_{\mathrm{fc}}\times C\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X{\circ }_{\mathrm{fc}}\times C\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$
22	20 21	mpbird	$$⊢\phi \to X{\circ }_{\mathrm{fc}}\times C\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$