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	|- ( ph -> P e. Prob )
	rrvmulc.2	|- ( ph -> X e. ( rRndVar ` P ) )
	rrvmulc.3	|- ( ph -> C e. RR )
Assertion	rrvmulc	|- ( ph -> ( X oFC x. C ) e. ( rRndVar ` P ) )

Proof

Step	Hyp	Ref	Expression
1		rrvmulc.1	|- ( ph -> P e. Prob )
2		rrvmulc.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		rrvmulc.3	|- ( ph -> C e. RR )
4	1 2	rrvvf	|- ( ph -> X : U. dom P --> RR )
5		domprobsiga	|- ( P e. Prob -> dom P e. U. ran sigAlgebra )
6	1 5	syl	|- ( ph -> dom P e. U. ran sigAlgebra )
7	6	uniexd	|- ( ph -> U. dom P e. _V )
8	4 7 3	ofcfval4	|- ( ph -> ( X oFC x. C ) = ( ( x e. RR |-> ( x x. C ) ) o. X ) )
9		brsigarn	|- BrSiga e. ( sigAlgebra ` RR )
10		elrnsiga	|- ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
11	9 10	mp1i	|- ( ph -> BrSiga e. U. ran sigAlgebra )
12	1	rrvmbfm	|- ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) )
13	2 12	mpbid	|- ( ph -> X e. ( dom P MblFnM BrSiga ) )
14		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
15	14 3	rmulccn	|- ( ph -> ( x e. RR |-> ( x x. C ) ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
16		df-brsiga	|- BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
17	16	a1i	|- ( ph -> BrSiga = ( sigaGen ` ( topGen ` ran (,) ) ) )
18	15 17 17	cnmbfm	|- ( ph -> ( x e. RR |-> ( x x. C ) ) e. ( BrSiga MblFnM BrSiga ) )
19	6 11 11 13 18	mbfmco	|- ( ph -> ( ( x e. RR |-> ( x x. C ) ) o. X ) e. ( dom P MblFnM BrSiga ) )
20	8 19	eqeltrd	|- ( ph -> ( X oFC x. C ) e. ( dom P MblFnM BrSiga ) )
21	1	rrvmbfm	|- ( ph -> ( ( X oFC x. C ) e. ( rRndVar ` P ) <-> ( X oFC x. C ) e. ( dom P MblFnM BrSiga ) ) )
22	20 21	mpbird	|- ( ph -> ( X oFC x. C ) e. ( rRndVar ` P ) )