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 
|- ( ph -> P e. Prob )
rrvadd.2 
|- ( ph -> X e. ( rRndVar ` P ) )
rrvadd.3 
|- ( ph -> Y e. ( rRndVar ` P ) )
Assertion rrvadd 
|- ( ph -> ( X oF + Y ) e. ( rRndVar ` P ) )

Proof

Step Hyp Ref Expression
1 rrvadd.1 
 |-  ( ph -> P e. Prob )
2 rrvadd.2 
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 rrvadd.3 
 |-  ( ph -> Y e. ( rRndVar ` P ) )
4 nfmpt1 
 |-  F/_ a ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. )
5 1 2 rrvvf 
 |-  ( ph -> X : U. dom P --> RR )
6 1 3 rrvvf 
 |-  ( ph -> Y : U. dom P --> RR )
7 1 unveldomd 
 |-  ( ph -> U. dom P e. dom P )
8 eqidd 
 |-  ( ph -> ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) = ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) )
9 eqidd 
 |-  ( ph -> ( x e. RR , y e. RR |-> ( x + y ) ) = ( x e. RR , y e. RR |-> ( x + y ) ) )
10 4 5 6 7 8 9 ofoprabco 
 |-  ( ph -> ( X oF + Y ) = ( ( x e. RR , y e. RR |-> ( x + y ) ) o. ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) ) )
11 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
12 1 11 syl 
 |-  ( ph -> dom P e. U. ran sigAlgebra )
13 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
14 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
15 13 14 mp1i 
 |-  ( ph -> BrSiga e. U. ran sigAlgebra )
16 sxsiga 
 |-  ( ( BrSiga e. U. ran sigAlgebra /\ BrSiga e. U. ran sigAlgebra ) -> ( BrSiga sX BrSiga ) e. U. ran sigAlgebra )
17 15 15 16 syl2anc 
 |-  ( ph -> ( BrSiga sX BrSiga ) e. U. ran sigAlgebra )
18 1 rrvmbfm 
 |-  ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) )
19 2 18 mpbid 
 |-  ( ph -> X e. ( dom P MblFnM BrSiga ) )
20 1 rrvmbfm 
 |-  ( ph -> ( Y e. ( rRndVar ` P ) <-> Y e. ( dom P MblFnM BrSiga ) ) )
21 3 20 mpbid 
 |-  ( ph -> Y e. ( dom P MblFnM BrSiga ) )
22 fveq2 
 |-  ( a = b -> ( X ` a ) = ( X ` b ) )
23 fveq2 
 |-  ( a = b -> ( Y ` a ) = ( Y ` b ) )
24 22 23 opeq12d 
 |-  ( a = b -> <. ( X ` a ) , ( Y ` a ) >. = <. ( X ` b ) , ( Y ` b ) >. )
25 24 cbvmptv 
 |-  ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) = ( b e. U. dom P |-> <. ( X ` b ) , ( Y ` b ) >. )
26 12 15 15 19 21 25 mbfmco2 
 |-  ( ph -> ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) e. ( dom P MblFnM ( BrSiga sX BrSiga ) ) )
27 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
28 27 raddcn 
 |-  ( x e. RR , y e. RR |-> ( x + y ) ) e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn ( topGen ` ran (,) ) )
29 28 a1i 
 |-  ( ph -> ( x e. RR , y e. RR |-> ( x + y ) ) e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn ( topGen ` ran (,) ) ) )
30 27 sxbrsiga 
 |-  ( BrSiga sX BrSiga ) = ( sigaGen ` ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) )
31 30 a1i 
 |-  ( ph -> ( BrSiga sX BrSiga ) = ( sigaGen ` ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) ) )
32 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
33 32 a1i 
 |-  ( ph -> BrSiga = ( sigaGen ` ( topGen ` ran (,) ) ) )
34 29 31 33 cnmbfm 
 |-  ( ph -> ( x e. RR , y e. RR |-> ( x + y ) ) e. ( ( BrSiga sX BrSiga ) MblFnM BrSiga ) )
35 12 17 15 26 34 mbfmco 
 |-  ( ph -> ( ( x e. RR , y e. RR |-> ( x + y ) ) o. ( a e. U. dom P |-> <. ( X ` a ) , ( Y ` a ) >. ) ) e. ( dom P MblFnM BrSiga ) )
36 10 35 eqeltrd 
 |-  ( ph -> ( X oF + Y ) e. ( dom P MblFnM BrSiga ) )
37 1 rrvmbfm 
 |-  ( ph -> ( ( X oF + Y ) e. ( rRndVar ` P ) <-> ( X oF + Y ) e. ( dom P MblFnM BrSiga ) ) )
38 36 37 mpbird 
 |-  ( ph -> ( X oF + Y ) e. ( rRndVar ` P ) )