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

Theorem 0rrv 24744
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  |-  ( ph  ->  P  e. Prob )
Assertion
Ref Expression
0rrv  |-  ( ph  ->  ( x  e.  U. dom  P  |->  0 )  e.  (rRndVar `  P )
)
Distinct variable group:    x, P
Allowed substitution hint:    ph( x)

Proof of Theorem 0rrv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 0re 9129 . . . . 5  |-  0  e.  RR
21rgenw 2780 . . . 4  |-  A. x  e.  U. dom  P 0  e.  RR
3 eqid 2443 . . . . 5  |-  ( x  e.  U. dom  P  |->  0 )  =  ( x  e.  U. dom  P 
|->  0 )
43fmpt 5926 . . . 4  |-  ( A. x  e.  U. dom  P
0  e.  RR  <->  ( x  e.  U. dom  P  |->  0 ) : U. dom  P --> RR )
52, 4mpbi 201 . . 3  |-  ( x  e.  U. dom  P  |->  0 ) : U. dom  P --> RR
65a1i 11 . 2  |-  ( ph  ->  ( x  e.  U. dom  P  |->  0 ) : U. dom  P --> RR )
7 fconstmpt 4956 . . . . . . . . . 10  |-  ( U. dom  P  X.  { 0 } )  =  ( x  e.  U. dom  P 
|->  0 )
87cnveqi 5082 . . . . . . . . 9  |-  `' ( U. dom  P  X.  { 0 } )  =  `' ( x  e.  U. dom  P  |->  0 )
9 cnvxp 5325 . . . . . . . . 9  |-  `' ( U. dom  P  X.  { 0 } )  =  ( { 0 }  X.  U. dom  P )
108, 9eqtr3i 2465 . . . . . . . 8  |-  `' ( x  e.  U. dom  P 
|->  0 )  =  ( { 0 }  X.  U.
dom  P )
1110imaeq1i 5235 . . . . . . 7  |-  ( `' ( x  e.  U. dom  P  |->  0 ) "
y )  =  ( ( { 0 }  X.  U. dom  P
) " y )
12 df-ima 4926 . . . . . . 7  |-  ( ( { 0 }  X.  U.
dom  P ) "
y )  =  ran  ( ( { 0 }  X.  U. dom  P )  |`  y )
13 df-rn 4924 . . . . . . 7  |-  ran  (
( { 0 }  X.  U. dom  P
)  |`  y )  =  dom  `' ( ( { 0 }  X.  U.
dom  P )  |`  y )
1411, 12, 133eqtri 2467 . . . . . 6  |-  ( `' ( x  e.  U. dom  P  |->  0 ) "
y )  =  dom  `' ( ( { 0 }  X.  U. dom  P )  |`  y )
15 df-res 4925 . . . . . . . . 9  |-  ( ( { 0 }  X.  U.
dom  P )  |`  y )  =  ( ( { 0 }  X.  U. dom  P
)  i^i  ( y  X.  _V ) )
16 inxp 5042 . . . . . . . . 9  |-  ( ( { 0 }  X.  U.
dom  P )  i^i  ( y  X.  _V ) )  =  ( ( { 0 }  i^i  y )  X.  ( U. dom  P  i^i  _V ) )
17 inv1 3642 . . . . . . . . . 10  |-  ( U. dom  P  i^i  _V )  =  U. dom  P
1817xpeq2i 4934 . . . . . . . . 9  |-  ( ( { 0 }  i^i  y )  X.  ( U. dom  P  i^i  _V ) )  =  ( ( { 0 }  i^i  y )  X. 
U. dom  P )
1915, 16, 183eqtri 2467 . . . . . . . 8  |-  ( ( { 0 }  X.  U.
dom  P )  |`  y )  =  ( ( { 0 }  i^i  y )  X. 
U. dom  P )
2019cnveqi 5082 . . . . . . 7  |-  `' ( ( { 0 }  X.  U. dom  P
)  |`  y )  =  `' ( ( { 0 }  i^i  y
)  X.  U. dom  P )
2120dmeqi 5106 . . . . . 6  |-  dom  `' ( ( { 0 }  X.  U. dom  P )  |`  y )  =  dom  `' ( ( { 0 }  i^i  y )  X.  U. dom  P )
22 cnvxp 5325 . . . . . . 7  |-  `' ( ( { 0 }  i^i  y )  X. 
U. dom  P )  =  ( U. dom  P  X.  ( { 0 }  i^i  y ) )
2322dmeqi 5106 . . . . . 6  |-  dom  `' ( ( { 0 }  i^i  y )  X.  U. dom  P
)  =  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )
2414, 21, 233eqtri 2467 . . . . 5  |-  ( `' ( x  e.  U. dom  P  |->  0 ) "
y )  =  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )
25 xpeq2 4928 . . . . . . . . . 10  |-  ( ( { 0 }  i^i  y )  =  (/)  ->  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  ( U. dom  P  X.  (/) ) )
26 xp0 5326 . . . . . . . . . 10  |-  ( U. dom  P  X.  (/) )  =  (/)
2725, 26syl6eq 2491 . . . . . . . . 9  |-  ( ( { 0 }  i^i  y )  =  (/)  ->  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  (/) )
2827dmeqd 5107 . . . . . . . 8  |-  ( ( { 0 }  i^i  y )  =  (/)  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  dom  (/) )
29 dm0 5118 . . . . . . . 8  |-  dom  (/)  =  (/)
3028, 29syl6eq 2491 . . . . . . 7  |-  ( ( { 0 }  i^i  y )  =  (/)  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  (/) )
3130adantl 454 . . . . . 6  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =  (/) )  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  (/) )
32 0rrv.1 . . . . . . . 8  |-  ( ph  ->  P  e. Prob )
33 domprobsiga 24704 . . . . . . . 8  |-  ( P  e. Prob  ->  dom  P  e.  U.
ran sigAlgebra )
34 0elsiga 24532 . . . . . . . 8  |-  ( dom 
P  e.  U. ran sigAlgebra  ->  (/)  e.  dom  P )
3532, 33, 343syl 19 . . . . . . 7  |-  ( ph  -> 
(/)  e.  dom  P )
3635adantr 453 . . . . . 6  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =  (/) )  ->  (/) 
e.  dom  P )
3731, 36eqeltrd 2517 . . . . 5  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =  (/) )  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  e.  dom  P )
3824, 37syl5eqel 2527 . . . 4  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =  (/) )  -> 
( `' ( x  e.  U. dom  P  |->  0 ) " y
)  e.  dom  P
)
39 dmxp 5123 . . . . . . 7  |-  ( ( { 0 }  i^i  y )  =/=  (/)  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  = 
U. dom  P )
4039adantl 454 . . . . . 6  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =/=  (/) )  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  =  U. dom  P
)
4132unveldomd 24708 . . . . . . 7  |-  ( ph  ->  U. dom  P  e. 
dom  P )
4241adantr 453 . . . . . 6  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =/=  (/) )  ->  U. dom  P  e.  dom  P )
4340, 42eqeltrd 2517 . . . . 5  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =/=  (/) )  ->  dom  ( U. dom  P  X.  ( { 0 }  i^i  y ) )  e.  dom  P )
4424, 43syl5eqel 2527 . . . 4  |-  ( (
ph  /\  ( {
0 }  i^i  y
)  =/=  (/) )  -> 
( `' ( x  e.  U. dom  P  |->  0 ) " y
)  e.  dom  P
)
4538, 44pm2.61dane 2689 . . 3  |-  ( ph  ->  ( `' ( x  e.  U. dom  P  |->  0 ) " y
)  e.  dom  P
)
4645ralrimivw 2797 . 2  |-  ( ph  ->  A. y  e. 𝔅  ( `' ( x  e.  U. dom  P  |->  0 ) " y
)  e.  dom  P
)
4732isrrvv 24736 . 2  |-  ( ph  ->  ( ( x  e. 
U. dom  P  |->  0 )  e.  (rRndVar `  P
)  <->  ( ( x  e.  U. dom  P  |->  0 ) : U. dom  P --> RR  /\  A. y  e. 𝔅  ( `' ( x  e.  U. dom  P  |->  0 ) " y
)  e.  dom  P
) ) )
486, 46, 47mpbir2and 890 1  |-  ( ph  ->  ( x  e.  U. dom  P  |->  0 )  e.  (rRndVar `  P )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1654    e. wcel 1728    =/= wne 2606   A.wral 2712   _Vcvv 2965    i^i cin 3308   (/)c0 3616   {csn 3843   U.cuni 4044    e. cmpt 4297    X. cxp 4911   `'ccnv 4912   dom cdm 4913   ran crn 4914    |` cres 4915   "cima 4916   -->wf 5485   ` cfv 5489   RRcr 9027   0cc0 9028  sigAlgebracsiga 24525  𝔅cbrsiga 24570  Probcprb 24700  rRndVarcrrv 24733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-i2m1 9096  ax-1ne0 9097  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-id 4533  df-po 4538  df-so 4539  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-er 6941  df-map 7056  df-en 7146  df-dom 7147  df-sdom 7148  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-ioo 10958  df-topgen 13705  df-top 17001  df-bases 17003  df-esum 24460  df-siga 24526  df-sigagen 24557  df-brsiga 24571  df-meas 24585  df-mbfm 24636  df-prob 24701  df-rrv 24734
  Copyright terms: Public domain W3C validator