Metamath Proof Explorer

Theorem sibf0

Description: The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018)

Ref Expression
Hypotheses sitgval.b 
|- B = ( Base ` W )
sitgval.j 
|- J = ( TopOpen ` W )
sitgval.s 
|- S = ( sigaGen ` J )
sitgval.0 
|- .0. = ( 0g ` W )
sitgval.x 
|- .x. = ( .s ` W )
sitgval.h 
|- H = ( RRHom ` ( Scalar ` W ) )
sitgval.1 
|- ( ph -> W e. V )
sitgval.2 
|- ( ph -> M e. U. ran measures )
sibf0.1 
|- ( ph -> W e. TopSp )
sibf0.2 
|- ( ph -> W e. Mnd )
Assertion sibf0 
|- ( ph -> ( U. dom M X. { .0. } ) e. dom ( W sitg M ) )

Proof

Step Hyp Ref Expression
1 sitgval.b 
 |-  B = ( Base ` W )
2 sitgval.j 
 |-  J = ( TopOpen ` W )
3 sitgval.s 
 |-  S = ( sigaGen ` J )
4 sitgval.0 
 |-  .0. = ( 0g ` W )
5 sitgval.x 
 |-  .x. = ( .s ` W )
6 sitgval.h 
 |-  H = ( RRHom ` ( Scalar ` W ) )
7 sitgval.1 
 |-  ( ph -> W e. V )
8 sitgval.2 
 |-  ( ph -> M e. U. ran measures )
9 sibf0.1 
 |-  ( ph -> W e. TopSp )
10 sibf0.2 
 |-  ( ph -> W e. Mnd )
11 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
12 8 11 syl 
 |-  ( ph -> dom M e. U. ran sigAlgebra )
13 2 fvexi 
 |-  J e. _V
14 13 a1i 
 |-  ( ph -> J e. _V )
15 14 sgsiga 
 |-  ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
16 3 15 eqeltrid 
 |-  ( ph -> S e. U. ran sigAlgebra )
17 fconstmpt 
 |-  ( U. dom M X. { .0. } ) = ( x e. U. dom M |-> .0. )
18 17 a1i 
 |-  ( ph -> ( U. dom M X. { .0. } ) = ( x e. U. dom M |-> .0. ) )
19 1 4 mndidcl 
 |-  ( W e. Mnd -> .0. e. B )
20 10 19 syl 
 |-  ( ph -> .0. e. B )
21 1 2 tpsuni 
 |-  ( W e. TopSp -> B = U. J )
22 9 21 syl 
 |-  ( ph -> B = U. J )
23 3 unieqi 
 |-  U. S = U. ( sigaGen ` J )
24 unisg 
 |-  ( J e. _V -> U. ( sigaGen ` J ) = U. J )
25 13 24 mp1i 
 |-  ( ph -> U. ( sigaGen ` J ) = U. J )
26 23 25 eqtrid 
 |-  ( ph -> U. S = U. J )
27 22 26 eqtr4d 
 |-  ( ph -> B = U. S )
28 20 27 eleqtrd 
 |-  ( ph -> .0. e. U. S )
29 12 16 18 28 mbfmcst 
 |-  ( ph -> ( U. dom M X. { .0. } ) e. ( dom M MblFnM S ) )
30 xpeq1 
 |-  ( U. dom M = (/) -> ( U. dom M X. { .0. } ) = ( (/) X. { .0. } ) )
31 0xp 
 |-  ( (/) X. { .0. } ) = (/)
32 30 31 eqtrdi 
 |-  ( U. dom M = (/) -> ( U. dom M X. { .0. } ) = (/) )
33 32 rneqd 
 |-  ( U. dom M = (/) -> ran ( U. dom M X. { .0. } ) = ran (/) )
34 rn0 
 |-  ran (/) = (/)
35 33 34 eqtrdi 
 |-  ( U. dom M = (/) -> ran ( U. dom M X. { .0. } ) = (/) )
36 0fi 
 |-  (/) e. Fin
37 35 36 eqeltrdi 
 |-  ( U. dom M = (/) -> ran ( U. dom M X. { .0. } ) e. Fin )
38 rnxp 
 |-  ( U. dom M =/= (/) -> ran ( U. dom M X. { .0. } ) = { .0. } )
39 snfi 
 |-  { .0. } e. Fin
40 38 39 eqeltrdi 
 |-  ( U. dom M =/= (/) -> ran ( U. dom M X. { .0. } ) e. Fin )
41 37 40 pm2.61ine 
 |-  ran ( U. dom M X. { .0. } ) e. Fin
42 41 a1i 
 |-  ( ph -> ran ( U. dom M X. { .0. } ) e. Fin )
43 noel 
 |-  -. x e. (/)
44 35 difeq1d 
 |-  ( U. dom M = (/) -> ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = ( (/) \ { .0. } ) )
45 0dif 
 |-  ( (/) \ { .0. } ) = (/)
46 44 45 eqtrdi 
 |-  ( U. dom M = (/) -> ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/) )
47 38 difeq1d 
 |-  ( U. dom M =/= (/) -> ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = ( { .0. } \ { .0. } ) )
48 difid 
 |-  ( { .0. } \ { .0. } ) = (/)
49 47 48 eqtrdi 
 |-  ( U. dom M =/= (/) -> ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/) )
50 46 49 pm2.61ine 
 |-  ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/)
51 50 eleq2i 
 |-  ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) <-> x e. (/) )
52 43 51 mtbir 
 |-  -. x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } )
53 52 pm2.21i 
 |-  ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) -> ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) e. ( 0 [,) +oo ) )
54 53 adantl 
 |-  ( ( ph /\ x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) ) -> ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) e. ( 0 [,) +oo ) )
55 54 ralrimiva 
 |-  ( ph -> A. x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) e. ( 0 [,) +oo ) )
56 1 2 3 4 5 6 7 8 issibf 
 |-  ( ph -> ( ( U. dom M X. { .0. } ) e. dom ( W sitg M ) <-> ( ( U. dom M X. { .0. } ) e. ( dom M MblFnM S ) /\ ran ( U. dom M X. { .0. } ) e. Fin /\ A. x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) e. ( 0 [,) +oo ) ) ) )
57 29 42 55 56 mpbir3and 
 |-  ( ph -> ( U. dom M X. { .0. } ) e. dom ( W sitg M ) )