Description: The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rrvadd.1 | |
|
rrvadd.2 | |
||
rrvadd.3 | |
||
Assertion | rrvadd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrvadd.1 | |
|
2 | rrvadd.2 | |
|
3 | rrvadd.3 | |
|
4 | nfmpt1 | |
|
5 | 1 2 | rrvvf | |
6 | 1 3 | rrvvf | |
7 | 1 | unveldomd | |
8 | eqidd | |
|
9 | eqidd | |
|
10 | 4 5 6 7 8 9 | ofoprabco | |
11 | domprobsiga | |
|
12 | 1 11 | syl | |
13 | brsigarn | |
|
14 | elrnsiga | |
|
15 | 13 14 | mp1i | |
16 | sxsiga | |
|
17 | 15 15 16 | syl2anc | |
18 | 1 | rrvmbfm | |
19 | 2 18 | mpbid | |
20 | 1 | rrvmbfm | |
21 | 3 20 | mpbid | |
22 | fveq2 | |
|
23 | fveq2 | |
|
24 | 22 23 | opeq12d | |
25 | 24 | cbvmptv | |
26 | 12 15 15 19 21 25 | mbfmco2 | |
27 | eqid | |
|
28 | 27 | raddcn | |
29 | 28 | a1i | |
30 | 27 | sxbrsiga | |
31 | 30 | a1i | |
32 | df-brsiga | |
|
33 | 32 | a1i | |
34 | 29 31 33 | cnmbfm | |
35 | 12 17 15 26 34 | mbfmco | |
36 | 10 35 | eqeltrd | |
37 | 1 | rrvmbfm | |
38 | 36 37 | mpbird | |