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 φ P Prob
rrvadd.2 φ X RndVar P
rrvadd.3 φ Y RndVar P
Assertion rrvadd φ X + f Y RndVar P

Proof

Step Hyp Ref Expression
1 rrvadd.1 φ P Prob
2 rrvadd.2 φ X RndVar P
3 rrvadd.3 φ Y RndVar P
4 nfmpt1 _ a a dom P X a Y a
5 1 2 rrvvf φ X : dom P
6 1 3 rrvvf φ Y : dom P
7 1 unveldomd φ dom P dom P
8 eqidd φ a dom P X a Y a = a dom P X a Y a
9 eqidd φ x , y x + y = x , y x + y
10 4 5 6 7 8 9 ofoprabco φ X + f Y = x , y x + y a dom P X a Y a
11 domprobsiga P Prob dom P ran sigAlgebra
12 1 11 syl φ dom P ran sigAlgebra
13 brsigarn 𝔅 sigAlgebra
14 elrnsiga 𝔅 sigAlgebra 𝔅 ran sigAlgebra
15 13 14 mp1i φ 𝔅 ran sigAlgebra
16 sxsiga 𝔅 ran sigAlgebra 𝔅 ran sigAlgebra 𝔅 × s 𝔅 ran sigAlgebra
17 15 15 16 syl2anc φ 𝔅 × s 𝔅 ran sigAlgebra
18 1 rrvmbfm φ X RndVar P X dom P MblFn μ 𝔅
19 2 18 mpbid φ X dom P MblFn μ 𝔅
20 1 rrvmbfm φ Y RndVar P Y dom P MblFn μ 𝔅
21 3 20 mpbid φ Y dom P MblFn μ 𝔅
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 dom P X a Y a = b dom P X b Y b
26 12 15 15 19 21 25 mbfmco2 φ a dom P X a Y a dom P MblFn μ 𝔅 × s 𝔅
27 eqid topGen ran . = topGen ran .
28 27 raddcn x , y x + y topGen ran . × t topGen ran . Cn topGen ran .
29 28 a1i φ x , y x + y topGen ran . × t topGen ran . Cn topGen ran .
30 27 sxbrsiga 𝔅 × s 𝔅 = 𝛔 topGen ran . × t topGen ran .
31 30 a1i φ 𝔅 × s 𝔅 = 𝛔 topGen ran . × t topGen ran .
32 df-brsiga 𝔅 = 𝛔 topGen ran .
33 32 a1i φ 𝔅 = 𝛔 topGen ran .
34 29 31 33 cnmbfm φ x , y x + y 𝔅 × s 𝔅 MblFn μ 𝔅
35 12 17 15 26 34 mbfmco φ x , y x + y a dom P X a Y a dom P MblFn μ 𝔅
36 10 35 eqeltrd φ X + f Y dom P MblFn μ 𝔅
37 1 rrvmbfm φ X + f Y RndVar P X + f Y dom P MblFn μ 𝔅
38 36 37 mpbird φ X + f Y RndVar P