Metamath Proof Explorer

Theorem issibf

Description: The predicate " F is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-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 )
Assertion issibf 
|- ( ph -> ( F e. dom ( W sitg M ) <-> ( F e. ( dom M MblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )

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 1 2 3 4 5 6 7 8 sitgval 
 |-  ( ph -> ( W sitg M ) = ( f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) ) )
10 9 dmeqd 
 |-  ( ph -> dom ( W sitg M ) = dom ( f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) ) )
11 eqid 
 |-  ( f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) ) = ( f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) )
12 11 dmmpt 
 |-  dom ( f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) ) = { f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } | ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) e. _V }
13 10 12 eqtrdi 
 |-  ( ph -> dom ( W sitg M ) = { f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } | ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) e. _V } )
14 13 eleq2d 
 |-  ( ph -> ( F e. dom ( W sitg M ) <-> F e. { f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } | ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) e. _V } ) )
15 rneq 
 |-  ( f = F -> ran f = ran F )
16 15 difeq1d 
 |-  ( f = F -> ( ran f \ { .0. } ) = ( ran F \ { .0. } ) )
17 cnveq 
 |-  ( f = F -> `' f = `' F )
18 17 imaeq1d 
 |-  ( f = F -> ( `' f " { x } ) = ( `' F " { x } ) )
19 18 fveq2d 
 |-  ( f = F -> ( M ` ( `' f " { x } ) ) = ( M ` ( `' F " { x } ) ) )
20 19 fveq2d 
 |-  ( f = F -> ( H ` ( M ` ( `' f " { x } ) ) ) = ( H ` ( M ` ( `' F " { x } ) ) ) )
21 20 oveq1d 
 |-  ( f = F -> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) = ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) )
22 16 21 mpteq12dv 
 |-  ( f = F -> ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) = ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) )
23 22 oveq2d 
 |-  ( f = F -> ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) = ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) )
24 23 eleq1d 
 |-  ( f = F -> ( ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) e. _V <-> ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V ) )
25 24 elrab 
 |-  ( F e. { f e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } | ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) e. _V } <-> ( F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } /\ ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V ) )
26 14 25 bitrdi 
 |-  ( ph -> ( F e. dom ( W sitg M ) <-> ( F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } /\ ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V ) ) )
27 ovex 
 |-  ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V
28 27 biantru 
 |-  ( F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } <-> ( F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } /\ ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V ) )
29 26 28 bitr4di 
 |-  ( ph -> ( F e. dom ( W sitg M ) <-> F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } ) )
30 rneq 
 |-  ( g = F -> ran g = ran F )
31 30 eleq1d 
 |-  ( g = F -> ( ran g e. Fin <-> ran F e. Fin ) )
32 30 difeq1d 
 |-  ( g = F -> ( ran g \ { .0. } ) = ( ran F \ { .0. } ) )
33 cnveq 
 |-  ( g = F -> `' g = `' F )
34 33 imaeq1d 
 |-  ( g = F -> ( `' g " { x } ) = ( `' F " { x } ) )
35 34 fveq2d 
 |-  ( g = F -> ( M ` ( `' g " { x } ) ) = ( M ` ( `' F " { x } ) ) )
36 35 eleq1d 
 |-  ( g = F -> ( ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) )
37 32 36 raleqbidv 
 |-  ( g = F -> ( A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) )
38 31 37 anbi12d 
 |-  ( g = F -> ( ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) <-> ( ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
39 38 elrab 
 |-  ( F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } <-> ( F e. ( dom M MblFnM S ) /\ ( ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
40 29 39 bitrdi 
 |-  ( ph -> ( F e. dom ( W sitg M ) <-> ( F e. ( dom M MblFnM S ) /\ ( ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) ) )
41 3anass 
 |-  ( ( F e. ( dom M MblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) <-> ( F e. ( dom M MblFnM S ) /\ ( ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
42 40 41 bitr4di 
 |-  ( ph -> ( F e. dom ( W sitg M ) <-> ( F e. ( dom M MblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )