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 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
rrvadd.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
rrvadd.3 ⊢ ( 𝜑 → 𝑌 ∈ ( rRndVar ‘ 𝑃 ) )
Assertion rrvadd ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ ( rRndVar ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 rrvadd.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 rrvadd.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 rrvadd.3 ⊢ ( 𝜑 → 𝑌 ∈ ( rRndVar ‘ 𝑃 ) )
4 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ )
5 1 2 rrvvf ⊢ ( 𝜑 → 𝑋 : ∪ dom 𝑃 ⟶ ℝ )
6 1 3 rrvvf ⊢ ( 𝜑 → 𝑌 : ∪ dom 𝑃 ⟶ ℝ )
7 1 unveldomd ⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )
8 eqidd ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) = ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) )
9 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) )
10 4 5 6 7 8 9 ofoprabco ⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∘ ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) ) )
11 domprobsiga ⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
12 1 11 syl ⊢ ( 𝜑 → dom 𝑃 ∈ ∪ 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 ⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
19 2 18 mpbid ⊢ ( 𝜑 → 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
20 1 rrvmbfm ⊢ ( 𝜑 → ( 𝑌 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑌 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
21 3 20 mpbid ⊢ ( 𝜑 → 𝑌 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
22 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑋 ‘ 𝑏 ) )
23 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝑏 ) )
24 22 23 opeq12d ⊢ ( 𝑎 = 𝑏 → ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ = ⟨ ( 𝑋 ‘ 𝑏 ) , ( 𝑌 ‘ 𝑏 ) ⟩ )
25 24 cbvmptv ⊢ ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) = ( 𝑏 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑏 ) , ( 𝑌 ‘ 𝑏 ) ⟩ )
26 12 15 15 19 21 25 mbfmco2 ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) ∈ ( dom 𝑃 MblFnM ( 𝔅ℝ ×s 𝔅ℝ ) ) )
27 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
28 27 raddcn ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn ( topGen ‘ ran (,) ) )
29 28 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn ( topGen ‘ ran (,) ) ) )
30 27 sxbrsiga ⊢ ( 𝔅ℝ ×s 𝔅ℝ ) = ( sigaGen ‘ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) )
31 30 a1i ⊢ ( 𝜑 → ( 𝔅ℝ ×s 𝔅ℝ ) = ( sigaGen ‘ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ) )
32 df-brsiga ⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
33 32 a1i ⊢ ( 𝜑 → 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
34 29 31 33 cnmbfm ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∈ ( ( 𝔅ℝ ×s 𝔅ℝ ) MblFnM 𝔅ℝ ) )
35 12 17 15 26 34 mbfmco ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∘ ( 𝑎 ∈ ∪ dom 𝑃 ↦ ⟨ ( 𝑋 ‘ 𝑎 ) , ( 𝑌 ‘ 𝑎 ) ⟩ ) ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
36 10 35 eqeltrd ⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
37 1 rrvmbfm ⊢ ( 𝜑 → ( ( 𝑋 ∘f + 𝑌 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 ∘f + 𝑌 ) ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
38 36 37 mpbird ⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ ( rRndVar ‘ 𝑃 ) )