Metamath Proof Explorer

Theorem sitgval

Description: Value of the simple function integral builder for a given space W and measure M . (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 )
Assertion 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 ) ) ) ) )

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 7 elexd 
 |-  ( ph -> W e. _V )
10 2fveq3 
 |-  ( w = W -> ( sigaGen ` ( TopOpen ` w ) ) = ( sigaGen ` ( TopOpen ` W ) ) )
11 2 fveq2i 
 |-  ( sigaGen ` J ) = ( sigaGen ` ( TopOpen ` W ) )
12 3 11 eqtri 
 |-  S = ( sigaGen ` ( TopOpen ` W ) )
13 10 12 eqtr4di 
 |-  ( w = W -> ( sigaGen ` ( TopOpen ` w ) ) = S )
14 13 oveq2d 
 |-  ( w = W -> ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) = ( dom m MblFnM S ) )
15 fveq2 
 |-  ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
16 15 4 eqtr4di 
 |-  ( w = W -> ( 0g ` w ) = .0. )
17 16 sneqd 
 |-  ( w = W -> { ( 0g ` w ) } = { .0. } )
18 17 difeq2d 
 |-  ( w = W -> ( ran g \ { ( 0g ` w ) } ) = ( ran g \ { .0. } ) )
19 18 raleqdv 
 |-  ( w = W -> ( A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) )
20 19 anbi2d 
 |-  ( w = W -> ( ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) <-> ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) ) )
21 14 20 rabeqbidv 
 |-  ( w = W -> { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } = { g e. ( dom m MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } )
22 id 
 |-  ( w = W -> w = W )
23 17 difeq2d 
 |-  ( w = W -> ( ran f \ { ( 0g ` w ) } ) = ( ran f \ { .0. } ) )
24 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
25 24 5 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
26 2fveq3 
 |-  ( w = W -> ( RRHom ` ( Scalar ` w ) ) = ( RRHom ` ( Scalar ` W ) ) )
27 26 6 eqtr4di 
 |-  ( w = W -> ( RRHom ` ( Scalar ` w ) ) = H )
28 27 fveq1d 
 |-  ( w = W -> ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) = ( H ` ( m ` ( `' f " { x } ) ) ) )
29 eqidd 
 |-  ( w = W -> x = x )
30 25 28 29 oveq123d 
 |-  ( w = W -> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) = ( ( H ` ( m ` ( `' f " { x } ) ) ) .x. x ) )
31 23 30 mpteq12dv 
 |-  ( w = W -> ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) = ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( m ` ( `' f " { x } ) ) ) .x. x ) ) )
32 22 31 oveq12d 
 |-  ( w = W -> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) = ( W gsum ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( m ` ( `' f " { x } ) ) ) .x. x ) ) ) )
33 21 32 mpteq12dv 
 |-  ( w = W -> ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) 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 ) ) ) ) )
34 dmeq 
 |-  ( m = M -> dom m = dom M )
35 34 oveq1d 
 |-  ( m = M -> ( dom m MblFnM S ) = ( dom M MblFnM S ) )
36 fveq1 
 |-  ( m = M -> ( m ` ( `' g " { x } ) ) = ( M ` ( `' g " { x } ) ) )
37 36 eleq1d 
 |-  ( m = M -> ( ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) )
38 37 ralbidv 
 |-  ( m = M -> ( A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) <-> A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) )
39 38 anbi2d 
 |-  ( m = M -> ( ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) <-> ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) ) )
40 35 39 rabeqbidv 
 |-  ( m = M -> { g e. ( dom m MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } = { g e. ( dom M MblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } )
41 simpl 
 |-  ( ( m = M /\ x e. ( ran f \ { .0. } ) ) -> m = M )
42 41 fveq1d 
 |-  ( ( m = M /\ x e. ( ran f \ { .0. } ) ) -> ( m ` ( `' f " { x } ) ) = ( M ` ( `' f " { x } ) ) )
43 42 fveq2d 
 |-  ( ( m = M /\ x e. ( ran f \ { .0. } ) ) -> ( H ` ( m ` ( `' f " { x } ) ) ) = ( H ` ( M ` ( `' f " { x } ) ) ) )
44 43 oveq1d 
 |-  ( ( m = M /\ x e. ( ran f \ { .0. } ) ) -> ( ( H ` ( m ` ( `' f " { x } ) ) ) .x. x ) = ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) )
45 44 mpteq2dva 
 |-  ( m = M -> ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( m ` ( `' f " { x } ) ) ) .x. x ) ) = ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) )
46 45 oveq2d 
 |-  ( m = M -> ( 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 ) ) ) )
47 40 46 mpteq12dv 
 |-  ( m = 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 ) ) ) ) = ( 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 ) ) ) ) )
48 df-sitg 
 |-  sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) )
49 ovex 
 |-  ( dom M MblFnM S ) e. _V
50 49 mptrabex 
 |-  ( 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
51 33 47 48 50 ovmpo 
 |-  ( ( W e. _V /\ M e. U. ran measures ) -> ( 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 ) ) ) ) )
52 9 8 51 syl2anc 
 |-  ( 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 ) ) ) ) )