Metamath Proof Explorer


Theorem rrvadd

Description: The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses rrvadd.1 φPProb
rrvadd.2 φXRndVarP
rrvadd.3 φYRndVarP
Assertion rrvadd φX+fYRndVarP

Proof

Step Hyp Ref Expression
1 rrvadd.1 φPProb
2 rrvadd.2 φXRndVarP
3 rrvadd.3 φYRndVarP
4 nfmpt1 _aadomPXaYa
5 1 2 rrvvf φX:domP
6 1 3 rrvvf φY:domP
7 1 unveldomd φdomPdomP
8 eqidd φadomPXaYa=adomPXaYa
9 eqidd φx,yx+y=x,yx+y
10 4 5 6 7 8 9 ofoprabco φX+fY=x,yx+yadomPXaYa
11 domprobsiga PProbdomPransigAlgebra
12 1 11 syl φdomPransigAlgebra
13 brsigarn 𝔅sigAlgebra
14 elrnsiga 𝔅sigAlgebra𝔅ransigAlgebra
15 13 14 mp1i φ𝔅ransigAlgebra
16 sxsiga 𝔅ransigAlgebra𝔅ransigAlgebra𝔅×s𝔅ransigAlgebra
17 15 15 16 syl2anc φ𝔅×s𝔅ransigAlgebra
18 1 rrvmbfm φXRndVarPXdomPMblFnμ𝔅
19 2 18 mpbid φXdomPMblFnμ𝔅
20 1 rrvmbfm φYRndVarPYdomPMblFnμ𝔅
21 3 20 mpbid φYdomPMblFnμ𝔅
22 fveq2 a=bXa=Xb
23 fveq2 a=bYa=Yb
24 22 23 opeq12d a=bXaYa=XbYb
25 24 cbvmptv adomPXaYa=bdomPXbYb
26 12 15 15 19 21 25 mbfmco2 φadomPXaYadomPMblFnμ𝔅×s𝔅
27 eqid topGenran.=topGenran.
28 27 raddcn x,yx+ytopGenran.×ttopGenran.CntopGenran.
29 28 a1i φx,yx+ytopGenran.×ttopGenran.CntopGenran.
30 27 sxbrsiga 𝔅×s𝔅=𝛔topGenran.×ttopGenran.
31 30 a1i φ𝔅×s𝔅=𝛔topGenran.×ttopGenran.
32 df-brsiga 𝔅=𝛔topGenran.
33 32 a1i φ𝔅=𝛔topGenran.
34 29 31 33 cnmbfm φx,yx+y𝔅×s𝔅MblFnμ𝔅
35 12 17 15 26 34 mbfmco φx,yx+yadomPXaYadomPMblFnμ𝔅
36 10 35 eqeltrd φX+fYdomPMblFnμ𝔅
37 1 rrvmbfm φX+fYRndVarPX+fYdomPMblFnμ𝔅
38 36 37 mpbird φX+fYRndVarP