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	$$⊢\phi \to P\in \mathrm{Prob}$$
	rrvadd.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	rrvadd.3	$$⊢\phi \to Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
Assertion	rrvadd	$$⊢\phi \to X{+}_{f}Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrvadd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		rrvadd.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3		rrvadd.3	$$⊢\phi \to Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
4		nfmpt1	$$⊢\underset{\_}{Ⅎ}a\left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)$$
5	1 2	rrvvf	$$⊢\phi \to X:\bigcup \mathrm{dom}P⟶ℝ$$
6	1 3	rrvvf	$$⊢\phi \to Y:\bigcup \mathrm{dom}P⟶ℝ$$
7	1	unveldomd	$$⊢\phi \to \bigcup \mathrm{dom}P\in \mathrm{dom}P$$
8		eqidd	$$⊢\phi \to \left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)=\left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)$$
9		eqidd	$$⊢\phi \to \left(x\in ℝ,y\in ℝ⟼x+y\right)=\left(x\in ℝ,y\in ℝ⟼x+y\right)$$
10	4 5 6 7 8 9	ofoprabco	$$⊢\phi \to X{+}_{f}Y=\left(x\in ℝ,y\in ℝ⟼x+y\right)\circ \left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)$$
11		domprobsiga	$$⊢P\in \mathrm{Prob}\to \mathrm{dom}P\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
12	1 11	syl	$$⊢\phi \to \mathrm{dom}P\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
13		brsigarn	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$$
14		elrnsiga	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)\to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
15	13 14	mp1i	$$⊢\phi \to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
16		sxsiga	$$⊢\left({𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
17	15 15 16	syl2anc	$$⊢\phi \to {𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
18	1	rrvmbfm	$$⊢\phi \to \left(X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$
19	2 18	mpbid	$$⊢\phi \to X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
20	1	rrvmbfm	$$⊢\phi \to \left(Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow Y\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$
21	3 20	mpbid	$$⊢\phi \to Y\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
22		fveq2	$$⊢a=b\to X\left(a\right)=X\left(b\right)$$
23		fveq2	$$⊢a=b\to Y\left(a\right)=Y\left(b\right)$$
24	22 23	opeq12d	$$⊢a=b\to ⟨X\left(a\right),Y\left(a\right)⟩=⟨X\left(b\right),Y\left(b\right)⟩$$
25	24	cbvmptv	$$⊢\left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)=\left(b\in \bigcup \mathrm{dom}P⟼⟨X\left(b\right),Y\left(b\right)⟩\right)$$
26	12 15 15 19 21 25	mbfmco2	$$⊢\phi \to \left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }\left({𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}\right)\right)$$
27		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
28	27	raddcn	$$⊢\left(x\in ℝ,y\in ℝ⟼x+y\right)\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\times }_t\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
29	28	a1i	$$⊢\phi \to \left(x\in ℝ,y\in ℝ⟼x+y\right)\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\times }_t\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
30	27	sxbrsiga	$$⊢{𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\times }_t\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
31	30	a1i	$$⊢\phi \to {𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\times }_t\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
32		df-brsiga	$$⊢{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
33	32	a1i	$$⊢\phi \to {𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
34	29 31 33	cnmbfm	$$⊢\phi \to \left(x\in ℝ,y\in ℝ⟼x+y\right)\in \left(\left({𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}\right){\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
35	12 17 15 26 34	mbfmco	$$⊢\phi \to \left(x\in ℝ,y\in ℝ⟼x+y\right)\circ \left(a\in \bigcup \mathrm{dom}P⟼⟨X\left(a\right),Y\left(a\right)⟩\right)\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
36	10 35	eqeltrd	$$⊢\phi \to X{+}_{f}Y\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
37	1	rrvmbfm	$$⊢\phi \to \left(X{+}_{f}Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X{+}_{f}Y\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$
38	36 37	mpbird	$$⊢\phi \to X{+}_{f}Y\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$