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 
|- ( ph -> P e. Prob )
Assertion 0rrv 
|- ( ph -> ( x e. U. dom P |-> 0 ) e. ( rRndVar ` P ) )

Proof

Step Hyp Ref Expression
1 0rrv.1 
 |-  ( ph -> P e. Prob )
2 0re 
 |-  0 e. RR
3 2 rgenw 
 |-  A. x e. U. dom P 0 e. RR
4 eqid 
 |-  ( x e. U. dom P |-> 0 ) = ( x e. U. dom P |-> 0 )
5 4 fmpt 
 |-  ( A. x e. U. dom P 0 e. RR <-> ( x e. U. dom P |-> 0 ) : U. dom P --> RR )
6 3 5 mpbi 
 |-  ( x e. U. dom P |-> 0 ) : U. dom P --> RR
7 6 a1i 
 |-  ( ph -> ( x e. U. dom P |-> 0 ) : U. dom P --> RR )
8 fconstmpt 
 |-  ( U. dom P X. { 0 } ) = ( x e. U. dom P |-> 0 )
9 8 cnveqi 
 |-  `' ( U. dom P X. { 0 } ) = `' ( x e. U. dom P |-> 0 )
10 cnvxp 
 |-  `' ( U. dom P X. { 0 } ) = ( { 0 } X. U. dom P )
11 9 10 eqtr3i 
 |-  `' ( x e. U. dom P |-> 0 ) = ( { 0 } X. U. dom P )
12 11 imaeq1i 
 |-  ( `' ( x e. U. dom P |-> 0 ) " y ) = ( ( { 0 } X. U. dom P ) " y )
13 df-ima 
 |-  ( ( { 0 } X. U. dom P ) " y ) = ran ( ( { 0 } X. U. dom P ) |` y )
14 df-rn 
 |-  ran ( ( { 0 } X. U. dom P ) |` y ) = dom `' ( ( { 0 } X. U. dom P ) |` y )
15 12 13 14 3eqtri 
 |-  ( `' ( x e. U. dom P |-> 0 ) " y ) = dom `' ( ( { 0 } X. U. dom P ) |` y )
16 df-res 
 |-  ( ( { 0 } X. U. dom P ) |` y ) = ( ( { 0 } X. U. dom P ) i^i ( y X. _V ) )
17 inxp 
 |-  ( ( { 0 } X. U. dom P ) i^i ( y X. _V ) ) = ( ( { 0 } i^i y ) X. ( U. dom P i^i _V ) )
18 inv1 
 |-  ( U. dom P i^i _V ) = U. dom P
19 18 xpeq2i 
 |-  ( ( { 0 } i^i y ) X. ( U. dom P i^i _V ) ) = ( ( { 0 } i^i y ) X. U. dom P )
20 16 17 19 3eqtri 
 |-  ( ( { 0 } X. U. dom P ) |` y ) = ( ( { 0 } i^i y ) X. U. dom P )
21 20 cnveqi 
 |-  `' ( ( { 0 } X. U. dom P ) |` y ) = `' ( ( { 0 } i^i y ) X. U. dom P )
22 21 dmeqi 
 |-  dom `' ( ( { 0 } X. U. dom P ) |` y ) = dom `' ( ( { 0 } i^i y ) X. U. dom P )
23 cnvxp 
 |-  `' ( ( { 0 } i^i y ) X. U. dom P ) = ( U. dom P X. ( { 0 } i^i y ) )
24 23 dmeqi 
 |-  dom `' ( ( { 0 } i^i y ) X. U. dom P ) = dom ( U. dom P X. ( { 0 } i^i y ) )
25 15 22 24 3eqtri 
 |-  ( `' ( x e. U. dom P |-> 0 ) " y ) = dom ( U. dom P X. ( { 0 } i^i y ) )
26 xpeq2 
 |-  ( ( { 0 } i^i y ) = (/) -> ( U. dom P X. ( { 0 } i^i y ) ) = ( U. dom P X. (/) ) )
27 xp0 
 |-  ( U. dom P X. (/) ) = (/)
28 26 27 eqtrdi 
 |-  ( ( { 0 } i^i y ) = (/) -> ( U. dom P X. ( { 0 } i^i y ) ) = (/) )
29 28 dmeqd 
 |-  ( ( { 0 } i^i y ) = (/) -> dom ( U. dom P X. ( { 0 } i^i y ) ) = dom (/) )
30 dm0 
 |-  dom (/) = (/)
31 29 30 eqtrdi 
 |-  ( ( { 0 } i^i y ) = (/) -> dom ( U. dom P X. ( { 0 } i^i y ) ) = (/) )
32 31 adantl 
 |-  ( ( ph /\ ( { 0 } i^i y ) = (/) ) -> dom ( U. dom P X. ( { 0 } i^i y ) ) = (/) )
33 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
34 0elsiga 
 |-  ( dom P e. U. ran sigAlgebra -> (/) e. dom P )
35 1 33 34 3syl 
 |-  ( ph -> (/) e. dom P )
36 35 adantr 
 |-  ( ( ph /\ ( { 0 } i^i y ) = (/) ) -> (/) e. dom P )
37 32 36 eqeltrd 
 |-  ( ( ph /\ ( { 0 } i^i y ) = (/) ) -> dom ( U. dom P X. ( { 0 } i^i y ) ) e. dom P )
38 25 37 eqeltrid 
 |-  ( ( ph /\ ( { 0 } i^i y ) = (/) ) -> ( `' ( x e. U. dom P |-> 0 ) " y ) e. dom P )
39 dmxp 
 |-  ( ( { 0 } i^i y ) =/= (/) -> dom ( U. dom P X. ( { 0 } i^i y ) ) = U. dom P )
40 39 adantl 
 |-  ( ( ph /\ ( { 0 } i^i y ) =/= (/) ) -> dom ( U. dom P X. ( { 0 } i^i y ) ) = U. dom P )
41 1 unveldomd 
 |-  ( ph -> U. dom P e. dom P )
42 41 adantr 
 |-  ( ( ph /\ ( { 0 } i^i y ) =/= (/) ) -> U. dom P e. dom P )
43 40 42 eqeltrd 
 |-  ( ( ph /\ ( { 0 } i^i y ) =/= (/) ) -> dom ( U. dom P X. ( { 0 } i^i y ) ) e. dom P )
44 25 43 eqeltrid 
 |-  ( ( ph /\ ( { 0 } i^i y ) =/= (/) ) -> ( `' ( x e. U. dom P |-> 0 ) " y ) e. dom P )
45 38 44 pm2.61dane 
 |-  ( ph -> ( `' ( x e. U. dom P |-> 0 ) " y ) e. dom P )
46 45 ralrimivw 
 |-  ( ph -> A. y e. BrSiga ( `' ( x e. U. dom P |-> 0 ) " y ) e. dom P )
47 1 isrrvv 
 |-  ( ph -> ( ( x e. U. dom P |-> 0 ) e. ( rRndVar ` P ) <-> ( ( x e. U. dom P |-> 0 ) : U. dom P --> RR /\ A. y e. BrSiga ( `' ( x e. U. dom P |-> 0 ) " y ) e. dom P ) ) )
48 7 46 47 mpbir2and 
 |-  ( ph -> ( x e. U. dom P |-> 0 ) e. ( rRndVar ` P ) )