Metamath Proof Explorer

Theorem sitgfval

Description: Value of the Bochner integral for a simple function F . (Contributed by Thierry Arnoux, 30-Jan-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 )
sibfmbl.1 
|- ( ph -> F e. dom ( W sitg M ) )
Assertion sitgfval 
|- ( ph -> ( ( W sitg M ) ` F ) = ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) )

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 sibfmbl.1 
 |-  ( ph -> F e. dom ( W sitg M ) )
10 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 ) ) ) ) )
11 simpr 
 |-  ( ( ph /\ f = F ) -> f = F )
12 11 rneqd 
 |-  ( ( ph /\ f = F ) -> ran f = ran F )
13 12 difeq1d 
 |-  ( ( ph /\ f = F ) -> ( ran f \ { .0. } ) = ( ran F \ { .0. } ) )
14 11 cnveqd 
 |-  ( ( ph /\ f = F ) -> `' f = `' F )
15 14 imaeq1d 
 |-  ( ( ph /\ f = F ) -> ( `' f " { x } ) = ( `' F " { x } ) )
16 15 fveq2d 
 |-  ( ( ph /\ f = F ) -> ( M ` ( `' f " { x } ) ) = ( M ` ( `' F " { x } ) ) )
17 16 fveq2d 
 |-  ( ( ph /\ f = F ) -> ( H ` ( M ` ( `' f " { x } ) ) ) = ( H ` ( M ` ( `' F " { x } ) ) ) )
18 17 oveq1d 
 |-  ( ( ph /\ f = F ) -> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) = ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) )
19 13 18 mpteq12dv 
 |-  ( ( ph /\ f = F ) -> ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) = ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) )
20 19 oveq2d 
 |-  ( ( ph /\ 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 ) ) ) )
21 1 2 3 4 5 6 7 8 9 sibfmbl 
 |-  ( ph -> F e. ( dom M MblFnM S ) )
22 1 2 3 4 5 6 7 8 9 sibfrn 
 |-  ( ph -> ran F e. Fin )
23 1 2 3 4 5 6 7 8 9 sibfima 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) )
24 23 ralrimiva 
 |-  ( ph -> A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) )
25 21 22 24 jca32 
 |-  ( ph -> ( F e. ( dom M MblFnM S ) /\ ( ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
26 rneq 
 |-  ( g = F -> ran g = ran F )
27 26 eleq1d 
 |-  ( g = F -> ( ran g e. Fin <-> ran F e. Fin ) )
28 26 difeq1d 
 |-  ( g = F -> ( ran g \ { .0. } ) = ( ran F \ { .0. } ) )
29 cnveq 
 |-  ( g = F -> `' g = `' F )
30 29 imaeq1d 
 |-  ( g = F -> ( `' g " { x } ) = ( `' F " { x } ) )
31 30 fveq2d 
 |-  ( g = F -> ( M ` ( `' g " { x } ) ) = ( M ` ( `' F " { x } ) ) )
32 31 eleq1d 
 |-  ( g = F -> ( ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) )
33 28 32 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 ) ) )
34 27 33 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 ) ) ) )
35 34 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 ) ) ) )
36 25 35 sylibr 
 |-  ( ph -> F e. { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } )
37 ovexd 
 |-  ( ph -> ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. _V )
38 10 20 36 37 fvmptd 
 |-  ( ph -> ( ( W sitg M ) ` F ) = ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) )