Metamath Proof Explorer

Theorem 0rrv

Description: The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017) (Revised by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypothesis 0rrv.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion 0rrv ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) ∈ ( rRndVar ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 0rrv.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 0re ⊢ 0 ∈ ℝ
3 2 rgenw ⊢ ∀ 𝑥 ∈ ∪ dom 𝑃 0 ∈ ℝ
4 eqid ⊢ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) = ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 )
5 4 fmpt ⊢ ( ∀ 𝑥 ∈ ∪ dom 𝑃 0 ∈ ℝ ↔ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) : ∪ dom 𝑃 ⟶ ℝ )
6 3 5 mpbi ⊢ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) : ∪ dom 𝑃 ⟶ ℝ
7 6 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) : ∪ dom 𝑃 ⟶ ℝ )
8 fconstmpt ⊢ ( ∪ dom 𝑃 × { 0 } ) = ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 )
9 8 cnveqi ⊢ ◡ ( ∪ dom 𝑃 × { 0 } ) = ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 )
10 cnvxp ⊢ ◡ ( ∪ dom 𝑃 × { 0 } ) = ( { 0 } × ∪ dom 𝑃 )
11 9 10 eqtr3i ⊢ ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) = ( { 0 } × ∪ dom 𝑃 )
12 11 imaeq1i ⊢ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) = ( ( { 0 } × ∪ dom 𝑃 ) “ 𝑦 )
13 df-ima ⊢ ( ( { 0 } × ∪ dom 𝑃 ) “ 𝑦 ) = ran ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 )
14 df-rn ⊢ ran ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = dom ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 )
15 12 13 14 3eqtri ⊢ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) = dom ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 )
16 df-res ⊢ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = ( ( { 0 } × ∪ dom 𝑃 ) ∩ ( 𝑦 × V ) )
17 inxp ⊢ ( ( { 0 } × ∪ dom 𝑃 ) ∩ ( 𝑦 × V ) ) = ( ( { 0 } ∩ 𝑦 ) × ( ∪ dom 𝑃 ∩ V ) )
18 inv1 ⊢ ( ∪ dom 𝑃 ∩ V ) = ∪ dom 𝑃
19 18 xpeq2i ⊢ ( ( { 0 } ∩ 𝑦 ) × ( ∪ dom 𝑃 ∩ V ) ) = ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
20 16 17 19 3eqtri ⊢ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
21 20 cnveqi ⊢ ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
22 21 dmeqi ⊢ dom ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = dom ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
23 cnvxp ⊢ ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 ) = ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
24 23 dmeqi ⊢ dom ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 ) = dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
25 15 22 24 3eqtri ⊢ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) = dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
26 xpeq2 ⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ( ∪ dom 𝑃 × ∅ ) )
27 xp0 ⊢ ( ∪ dom 𝑃 × ∅ ) = ∅
28 26 27 eqtrdi ⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
29 28 dmeqd ⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = dom ∅ )
30 dm0 ⊢ dom ∅ = ∅
31 29 30 eqtrdi ⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
32 31 adantl ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
33 domprobsiga ⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
34 0elsiga ⊢ ( dom 𝑃 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑃 )
35 1 33 34 3syl ⊢ ( 𝜑 → ∅ ∈ dom 𝑃 )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → ∅ ∈ dom 𝑃 )
37 32 36 eqeltrd ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) ∈ dom 𝑃 )
38 25 37 eqeltrid ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
39 dmxp ⊢ ( ( { 0 } ∩ 𝑦 ) ≠ ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∪ dom 𝑃 )
40 39 adantl ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∪ dom 𝑃 )
41 1 unveldomd ⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → ∪ dom 𝑃 ∈ dom 𝑃 )
43 40 42 eqeltrd ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) ∈ dom 𝑃 )
44 25 43 eqeltrid ⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
45 38 44 pm2.61dane ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
46 45 ralrimivw ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝔅ℝ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
47 1 isrrvv ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 ) ) )
48 7 46 47 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) ∈ ( rRndVar ‘ 𝑃 ) )