Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  0rrv Structured version   Visualization version   GIF version

Theorem 0rrv 30743
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.
StepHypRef Expression
1 0re 10153 . . . . 5 0 ∈ ℝ
21rgenw 3026 . . . 4 𝑥 dom 𝑃0 ∈ ℝ
3 eqid 2724 . . . . 5 (𝑥 dom 𝑃 ↦ 0) = (𝑥 dom 𝑃 ↦ 0)
43fmpt 6496 . . . 4 (∀𝑥 dom 𝑃0 ∈ ℝ ↔ (𝑥 dom 𝑃 ↦ 0): dom 𝑃⟶ℝ)
52, 4mpbi 220 . . 3 (𝑥 dom 𝑃 ↦ 0): dom 𝑃⟶ℝ
65a1i 11 . 2 (𝜑 → (𝑥 dom 𝑃 ↦ 0): dom 𝑃⟶ℝ)
7 fconstmpt 5272 . . . . . . . . . 10 ( dom 𝑃 × {0}) = (𝑥 dom 𝑃 ↦ 0)
87cnveqi 5404 . . . . . . . . 9 ( dom 𝑃 × {0}) = (𝑥 dom 𝑃 ↦ 0)
9 cnvxp 5661 . . . . . . . . 9 ( dom 𝑃 × {0}) = ({0} × dom 𝑃)
108, 9eqtr3i 2748 . . . . . . . 8 (𝑥 dom 𝑃 ↦ 0) = ({0} × dom 𝑃)
1110imaeq1i 5573 . . . . . . 7 ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) = (({0} × dom 𝑃) “ 𝑦)
12 df-ima 5231 . . . . . . 7 (({0} × dom 𝑃) “ 𝑦) = ran (({0} × dom 𝑃) ↾ 𝑦)
13 df-rn 5229 . . . . . . 7 ran (({0} × dom 𝑃) ↾ 𝑦) = dom (({0} × dom 𝑃) ↾ 𝑦)
1411, 12, 133eqtri 2750 . . . . . 6 ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) = dom (({0} × dom 𝑃) ↾ 𝑦)
15 df-res 5230 . . . . . . . . 9 (({0} × dom 𝑃) ↾ 𝑦) = (({0} × dom 𝑃) ∩ (𝑦 × V))
16 inxp 5362 . . . . . . . . 9 (({0} × dom 𝑃) ∩ (𝑦 × V)) = (({0} ∩ 𝑦) × ( dom 𝑃 ∩ V))
17 inv1 4078 . . . . . . . . . 10 ( dom 𝑃 ∩ V) = dom 𝑃
1817xpeq2i 5245 . . . . . . . . 9 (({0} ∩ 𝑦) × ( dom 𝑃 ∩ V)) = (({0} ∩ 𝑦) × dom 𝑃)
1915, 16, 183eqtri 2750 . . . . . . . 8 (({0} × dom 𝑃) ↾ 𝑦) = (({0} ∩ 𝑦) × dom 𝑃)
2019cnveqi 5404 . . . . . . 7 (({0} × dom 𝑃) ↾ 𝑦) = (({0} ∩ 𝑦) × dom 𝑃)
2120dmeqi 5432 . . . . . 6 dom (({0} × dom 𝑃) ↾ 𝑦) = dom (({0} ∩ 𝑦) × dom 𝑃)
22 cnvxp 5661 . . . . . . 7 (({0} ∩ 𝑦) × dom 𝑃) = ( dom 𝑃 × ({0} ∩ 𝑦))
2322dmeqi 5432 . . . . . 6 dom (({0} ∩ 𝑦) × dom 𝑃) = dom ( dom 𝑃 × ({0} ∩ 𝑦))
2414, 21, 233eqtri 2750 . . . . 5 ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) = dom ( dom 𝑃 × ({0} ∩ 𝑦))
25 xpeq2 5238 . . . . . . . . . 10 (({0} ∩ 𝑦) = ∅ → ( dom 𝑃 × ({0} ∩ 𝑦)) = ( dom 𝑃 × ∅))
26 xp0 5662 . . . . . . . . . 10 ( dom 𝑃 × ∅) = ∅
2725, 26syl6eq 2774 . . . . . . . . 9 (({0} ∩ 𝑦) = ∅ → ( dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
2827dmeqd 5433 . . . . . . . 8 (({0} ∩ 𝑦) = ∅ → dom ( dom 𝑃 × ({0} ∩ 𝑦)) = dom ∅)
29 dm0 5446 . . . . . . . 8 dom ∅ = ∅
3028, 29syl6eq 2774 . . . . . . 7 (({0} ∩ 𝑦) = ∅ → dom ( dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
3130adantl 473 . . . . . 6 ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom ( dom 𝑃 × ({0} ∩ 𝑦)) = ∅)
32 0rrv.1 . . . . . . . 8 (𝜑𝑃 ∈ Prob)
33 domprobsiga 30703 . . . . . . . 8 (𝑃 ∈ Prob → dom 𝑃 ran sigAlgebra)
34 0elsiga 30407 . . . . . . . 8 (dom 𝑃 ran sigAlgebra → ∅ ∈ dom 𝑃)
3532, 33, 343syl 18 . . . . . . 7 (𝜑 → ∅ ∈ dom 𝑃)
3635adantr 472 . . . . . 6 ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → ∅ ∈ dom 𝑃)
3731, 36eqeltrd 2803 . . . . 5 ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom ( dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃)
3824, 37syl5eqel 2807 . . . 4 ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
39 dmxp 5451 . . . . . . 7 (({0} ∩ 𝑦) ≠ ∅ → dom ( dom 𝑃 × ({0} ∩ 𝑦)) = dom 𝑃)
4039adantl 473 . . . . . 6 ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom ( dom 𝑃 × ({0} ∩ 𝑦)) = dom 𝑃)
4132unveldomd 30707 . . . . . . 7 (𝜑 dom 𝑃 ∈ dom 𝑃)
4241adantr 472 . . . . . 6 ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom 𝑃 ∈ dom 𝑃)
4340, 42eqeltrd 2803 . . . . 5 ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom ( dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃)
4424, 43syl5eqel 2807 . . . 4 ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
4538, 44pm2.61dane 2983 . . 3 (𝜑 → ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
4645ralrimivw 3069 . 2 (𝜑 → ∀𝑦 ∈ 𝔅 ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)
4732isrrvv 30735 . 2 (𝜑 → ((𝑥 dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃) ↔ ((𝑥 dom 𝑃 ↦ 0): dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅 ((𝑥 dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃)))
486, 46, 47mpbir2and 995 1 (𝜑 → (𝑥 dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1596  wcel 2103  wne 2896  wral 3014  Vcvv 3304  cin 3679  c0 4023  {csn 4285   cuni 4544  cmpt 4837   × cxp 5216  ccnv 5217  dom cdm 5218  ran crn 5219  cres 5220  cima 5221  wf 5997  cfv 6001  cr 10048  0cc0 10049  sigAlgebracsiga 30400  𝔅cbrsiga 30474  Probcprb 30699  rRndVarcrrv 30732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-i2m1 10117  ax-1ne0 10118  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-po 5139  df-so 5140  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-1st 7285  df-2nd 7286  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-ioo 12293  df-topgen 16227  df-top 20822  df-bases 20873  df-esum 30320  df-siga 30401  df-sigagen 30432  df-brsiga 30475  df-meas 30489  df-mbfm 30543  df-prob 30700  df-rrv 30733
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator