Metamath Proof Explorer

Theorem sitgf

Description: The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-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 )
sitgf.1 
|- ( ( ph /\ f e. dom ( W sitg M ) ) -> ( ( W sitg M ) ` f ) e. B )
Assertion sitgf 
|- ( ph -> ( W sitg M ) : dom ( W sitg M ) --> B )

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 sitgf.1 
 |-  ( ( ph /\ f e. dom ( W sitg M ) ) -> ( ( W sitg M ) ` f ) e. B )
10 funmpt 
 |-  Fun ( 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 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 ) ) ) ) )
12 11 funeqd 
 |-  ( ph -> ( Fun ( W sitg M ) <-> Fun ( 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 ) ) ) ) ) )
13 10 12 mpbiri 
 |-  ( ph -> Fun ( W sitg M ) )
14 13 funfnd 
 |-  ( ph -> ( W sitg M ) Fn dom ( W sitg M ) )
15 9 ralrimiva 
 |-  ( ph -> A. f e. dom ( W sitg M ) ( ( W sitg M ) ` f ) e. B )
16 fnfvrnss 
 |-  ( ( ( W sitg M ) Fn dom ( W sitg M ) /\ A. f e. dom ( W sitg M ) ( ( W sitg M ) ` f ) e. B ) -> ran ( W sitg M ) C_ B )
17 14 15 16 syl2anc 
 |-  ( ph -> ran ( W sitg M ) C_ B )
18 df-f 
 |-  ( ( W sitg M ) : dom ( W sitg M ) --> B <-> ( ( W sitg M ) Fn dom ( W sitg M ) /\ ran ( W sitg M ) C_ B ) )
19 14 17 18 sylanbrc 
 |-  ( ph -> ( W sitg M ) : dom ( W sitg M ) --> B )