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		xpres	⊢ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
17	16	cnveqi	⊢ ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
18	17	dmeqi	⊢ dom ◡ ( ( { 0 } × ∪ dom 𝑃 ) ↾ 𝑦 ) = dom ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 )
19		cnvxp	⊢ ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 ) = ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
20	19	dmeqi	⊢ dom ◡ ( ( { 0 } ∩ 𝑦 ) × ∪ dom 𝑃 ) = dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
21	15 18 20	3eqtri	⊢ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) = dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) )
22		xpeq2	⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ( ∪ dom 𝑃 × ∅ ) )
23		xp0	⊢ ( ∪ dom 𝑃 × ∅ ) = ∅
24	22 23	eqtrdi	⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
25	24	dmeqd	⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = dom ∅ )
26		dm0	⊢ dom ∅ = ∅
27	25 26	eqtrdi	⊢ ( ( { 0 } ∩ 𝑦 ) = ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
28	27	adantl	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∅ )
29		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
30		0elsiga	⊢ ( dom 𝑃 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑃 )
31	1 29 30	3syl	⊢ ( 𝜑 → ∅ ∈ dom 𝑃 )
32	31	adantr	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → ∅ ∈ dom 𝑃 )
33	28 32	eqeltrd	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) ∈ dom 𝑃 )
34	21 33	eqeltrid	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) = ∅ ) → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
35		dmxp	⊢ ( ( { 0 } ∩ 𝑦 ) ≠ ∅ → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∪ dom 𝑃 )
36	35	adantl	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) = ∪ dom 𝑃 )
37	1	unveldomd	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )
38	37	adantr	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → ∪ dom 𝑃 ∈ dom 𝑃 )
39	36 38	eqeltrd	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ dom 𝑃 × ( { 0 } ∩ 𝑦 ) ) ∈ dom 𝑃 )
40	21 39	eqeltrid	⊢ ( ( 𝜑 ∧ ( { 0 } ∩ 𝑦 ) ≠ ∅ ) → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
41	34 40	pm2.61dane	⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
42	41	ralrimivw	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝔅ℝ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 )
43	1	isrrvv	⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) “ 𝑦 ) ∈ dom 𝑃 ) ) )
44	7 42 43	mpbir2and	⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↦ 0 ) ∈ ( rRndVar ‘ 𝑃 ) )