Theorem 0rrv 32360

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.)

Hypothesis

Ref	Expression
0rrv.1	⊢ (𝜑 → 𝑃 ∈ Prob)

Assertion

Ref	Expression
0rrv	⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃))

Distinct variable group:   𝑥,𝑃

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 0rrv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0re 10924	. . . . 5 ⊢ 0 ∈ ℝ
2	1	rgenw 3074	. . . 4 ⊢ ∀𝑥 ∈ ∪ dom 𝑃0 ∈ ℝ
3		eqid 2737	. . . . 5 ⊢ (𝑥 ∈ ∪ dom 𝑃 ↦ 0) = (𝑥 ∈ ∪ dom 𝑃 ↦ 0)
4	3	fmpt 6971	. . . 4 ⊢ (∀𝑥 ∈ ∪ dom 𝑃0 ∈ ℝ ↔ (𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom 𝑃⟶ℝ)
5	2, 4	mpbi 229	. . 3 ⊢ (𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom 𝑃⟶ℝ
6	5	a1i 11	. 2 ⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom 𝑃⟶ℝ)
7		fconstmpt 5645	. . . . . . . . . 10 ⊢ (∪ dom 𝑃 × {0}) = (𝑥 ∈ ∪ dom 𝑃 ↦ 0)
8	7	cnveqi 5777	. . . . . . . . 9 ⊢ ◡(∪ dom 𝑃 × {0}) = ◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0)
9		cnvxp 6054	. . . . . . . . 9 ⊢ ◡(∪ dom 𝑃 × {0}) = ({0} × ∪ dom 𝑃)
10	8, 9	eqtr3i 2767	. . . . . . . 8 ⊢ ◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) = ({0} × ∪ dom 𝑃)
11	10	imaeq1i 5960	. . . . . . 7 ⊢ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) = (({0} × ∪ dom 𝑃) “ 𝑦)
12		df-ima 5598	. . . . . . 7 ⊢ (({0} × ∪ dom 𝑃) “ 𝑦) = ran (({0} × ∪ dom 𝑃) ↾ 𝑦)
13		df-rn 5596	. . . . . . 7 ⊢ ran (({0} × ∪ dom 𝑃) ↾ 𝑦) = dom ◡(({0} × ∪ dom 𝑃) ↾ 𝑦)
14	11, 12, 13	3eqtri 2769	. . . . . 6 ⊢ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) = dom ◡(({0} × ∪ dom 𝑃) ↾ 𝑦)
15		df-res 5597	. . . . . . . . 9 ⊢ (({0} × ∪ dom 𝑃) ↾ 𝑦) = (({0} × ∪ dom 𝑃) ∩ (𝑦 × V))
16		inxp 5735	. . . . . . . . 9 ⊢ (({0} × ∪ dom 𝑃) ∩ (𝑦 × V)) = (({0} ∩ 𝑦) × (∪ dom 𝑃 ∩ V))
17		inv1 4330	. . . . . . . . . 10 ⊢ (∪ dom 𝑃 ∩ V) = ∪ dom 𝑃
18	17	xpeq2i 5612	. . . . . . . . 9 ⊢ (({0} ∩ 𝑦) × (∪ dom 𝑃 ∩ V)) = (({0} ∩ 𝑦) × ∪ dom 𝑃)
19	15, 16, 18	3eqtri 2769	. . . . . . . 8 ⊢ (({0} × ∪ dom 𝑃) ↾ 𝑦) = (({0} ∩ 𝑦) × ∪ dom 𝑃)
20	19	cnveqi 5777	. . . . . . 7 ⊢ ◡(({0} × ∪ dom 𝑃) ↾ 𝑦) = ◡(({0} ∩ 𝑦) × ∪ dom 𝑃)
21	20	dmeqi 5807	. . . . . 6 ⊢ dom ◡(({0} × ∪ dom 𝑃) ↾ 𝑦) = dom ◡(({0} ∩ 𝑦) × ∪ dom 𝑃)
22		cnvxp 6054	. . . . . . 7 ⊢ ◡(({0} ∩ 𝑦) × ∪ dom 𝑃) = (∪ dom 𝑃 × ({0} ∩ 𝑦))
23	22	dmeqi 5807	. . . . . 6 ⊢ dom ◡(({0} ∩ 𝑦) × ∪ dom 𝑃) = dom (∪ dom 𝑃 × ({0} ∩ 𝑦))
24	14, 21, 23	3eqtri 2769	. . . . 5 ⊢ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) = dom (∪ dom 𝑃 × ({0} ∩ 𝑦))
25		xpeq2 5606	. . . . . . . . . 10 ⊢ (({0} ∩ 𝑦) = ∅ → (∪ dom 𝑃 × ({0} ∩ 𝑦)) = (∪ dom 𝑃 × ∅))
26		xp0 6055	. . . . . . . . . 10 ⊢ (∪ dom 𝑃 × ∅) = ∅
27	25, 26	eqtrdi 2793	. . . . . . . . 9 ⊢ (({0} ∩ 𝑦) = ∅ → (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
28	27	dmeqd 5808	. . . . . . . 8 ⊢ (({0} ∩ 𝑦) = ∅ → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = dom ∅)
29		dm0 5823	. . . . . . . 8 ⊢ dom ∅ = ∅
30	28, 29	eqtrdi 2793	. . . . . . 7 ⊢ (({0} ∩ 𝑦) = ∅ → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
31	30	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
32		0rrv.1	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ Prob)
33		domprobsiga 32320	. . . . . . . 8 ⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra)
34		0elsiga 32024	. . . . . . . 8 ⊢ (dom 𝑃 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑃)
35	32, 33, 34	3syl 18	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ dom 𝑃)
36	35	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → ∅ ∈ dom 𝑃)
37	31, 36	eqeltrd 2837	. . . . 5 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃)
38	24, 37	eqeltrid 2841	. . . 4 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
39		dmxp 5832	. . . . . . 7 ⊢ (({0} ∩ 𝑦) ≠ ∅ → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∪ dom 𝑃)
40	39	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∪ dom 𝑃)
41	32	unveldomd 32324	. . . . . . 7 ⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃)
42	41	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → ∪ dom 𝑃 ∈ dom 𝑃)
43	40, 42	eqeltrd 2837	. . . . 5 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃)
44	24, 43	eqeltrid 2841	. . . 4 ⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
45	38, 44	pm2.61dane 3030	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
46	45	ralrimivw 3107	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝔅ℝ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
47	32	isrrvv 32352	. 2 ⊢ (𝜑 → ((𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃) ↔ ((𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅ℝ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)))
48	6, 46, 47	mpbir2and 709	1 ⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  Vcvv 3427   ∩ cin 3887  ∅c0 4258  {csn 4563  ∪ cuni 4841   ↦ cmpt 5158   × cxp 5583  ^◡ccnv 5584  dom cdm 5585  ran crn 5586   ↾ cres 5587   “ cima 5588  ⟶wf 6419  ‘cfv 6423  ℝcr 10817  0cc0 10818  sigAlgebracsiga 32018  𝔅_ℝcbrsiga 32091  Probcprb 32316  rRndVarcrrv 32349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-addrcl 10879  ax-rnegex 10889  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-int 4882  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-po 5499  df-so 5500  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-ov 7263  df-oprab 7264  df-mpo 7265  df-1st 7809  df-2nd 7810  df-er 8461  df-map 8580  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-ioo 13028  df-topgen 17098  df-top 21987  df-bases 22040  df-esum 31938  df-siga 32019  df-sigagen 32049  df-brsiga 32092  df-meas 32106  df-mbfm 32160  df-prob 32317  df-rrv 32350

This theorem is referenced by: (None)