Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sitgfval Structured version   Unicode version

Theorem sitgfval 29002
Description: Value of the Bochner integral for a simple function  F. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypotheses
Ref Expression
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  ( Wsitg M ) )
Assertion
Ref Expression
sitgfval  |-  ( ph  ->  ( ( Wsitg M
) `  F )  =  ( W  gsumg  ( x  e.  ( ran  F  \  {  .0.  } ) 
|->  ( ( H `  ( M `  ( `' F " { x } ) ) ) 
.x.  x ) ) ) )
Distinct variable groups:    x, F    x, M    x, W    x,  .0.   
ph, x
Allowed substitution hints:    B( x)    S( x)    .x. ( x)    H( x)    J( x)    V( x)

Proof of Theorem sitgfval
Dummy variables  f 
g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sitgval.b . . 3  |-  B  =  ( Base `  W
)
2 sitgval.j . . 3  |-  J  =  ( TopOpen `  W )
3 sitgval.s . . 3  |-  S  =  (sigaGen `  J )
4 sitgval.0 . . 3  |-  .0.  =  ( 0g `  W )
5 sitgval.x . . 3  |-  .x.  =  ( .s `  W )
6 sitgval.h . . 3  |-  H  =  (RRHom `  (Scalar `  W
) )
7 sitgval.1 . . 3  |-  ( ph  ->  W  e.  V )
8 sitgval.2 . . 3  |-  ( ph  ->  M  e.  U. ran measures )
91, 2, 3, 4, 5, 6, 7, 8sitgval 28993 . 2  |-  ( ph  ->  ( Wsitg M )  =  ( f  e. 
{ g  e.  ( dom  MMblFnM S )  |  ( ran  g  e. 
Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( M `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( W  gsumg  ( x  e.  ( ran  f  \  {  .0.  } )  |->  ( ( H `  ( M `
 ( `' f
" { x }
) ) )  .x.  x ) ) ) ) )
10 simpr 462 . . . . . 6  |-  ( (
ph  /\  f  =  F )  ->  f  =  F )
1110rneqd 5082 . . . . 5  |-  ( (
ph  /\  f  =  F )  ->  ran  f  =  ran  F )
1211difeq1d 3588 . . . 4  |-  ( (
ph  /\  f  =  F )  ->  ( ran  f  \  {  .0.  } )  =  ( ran 
F  \  {  .0.  } ) )
1310cnveqd 5030 . . . . . . . 8  |-  ( (
ph  /\  f  =  F )  ->  `' f  =  `' F
)
1413imaeq1d 5187 . . . . . . 7  |-  ( (
ph  /\  f  =  F )  ->  ( `' f " {
x } )  =  ( `' F " { x } ) )
1514fveq2d 5885 . . . . . 6  |-  ( (
ph  /\  f  =  F )  ->  ( M `  ( `' f " { x }
) )  =  ( M `  ( `' F " { x } ) ) )
1615fveq2d 5885 . . . . 5  |-  ( (
ph  /\  f  =  F )  ->  ( H `  ( M `  ( `' f " { x } ) ) )  =  ( H `  ( M `
 ( `' F " { x } ) ) ) )
1716oveq1d 6320 . . . 4  |-  ( (
ph  /\  f  =  F )  ->  (
( H `  ( M `  ( `' f " { x }
) ) )  .x.  x )  =  ( ( H `  ( M `  ( `' F " { x }
) ) )  .x.  x ) )
1812, 17mpteq12dv 4504 . . 3  |-  ( (
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 ) ) )
1918oveq2d 6321 . 2  |-  ( (
ph  /\  f  =  F )  ->  ( W  gsumg  ( x  e.  ( ran  f  \  {  .0.  } )  |->  ( ( H `  ( M `
 ( `' f
" { x }
) ) )  .x.  x ) ) )  =  ( W  gsumg  ( x  e.  ( ran  F  \  {  .0.  } ) 
|->  ( ( H `  ( M `  ( `' F " { x } ) ) ) 
.x.  x ) ) ) )
20 sibfmbl.1 . . . . 5  |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )
211, 2, 3, 4, 5, 6, 7, 8, 20sibfmbl 28996 . . . 4  |-  ( ph  ->  F  e.  ( dom 
MMblFnM S ) )
221, 2, 3, 4, 5, 6, 7, 8, 20sibfrn 28998 . . . 4  |-  ( ph  ->  ran  F  e.  Fin )
231, 2, 3, 4, 5, 6, 7, 8, 20sibfima 28999 . . . . 5  |-  ( (
ph  /\  x  e.  ( ran  F  \  {  .0.  } ) )  -> 
( M `  ( `' F " { x } ) )  e.  ( 0 [,) +oo ) )
2423ralrimiva 2846 . . . 4  |-  ( ph  ->  A. x  e.  ( ran  F  \  {  .0.  } ) ( M `
 ( `' F " { x } ) )  e.  ( 0 [,) +oo ) )
2521, 22, 24jca32 537 . . 3  |-  ( ph  ->  ( F  e.  ( dom  MMblFnM S )  /\  ( ran  F  e.  Fin  /\ 
A. x  e.  ( ran  F  \  {  .0.  } ) ( M `
 ( `' F " { x } ) )  e.  ( 0 [,) +oo ) ) ) )
26 rneq 5080 . . . . . 6  |-  ( g  =  F  ->  ran  g  =  ran  F )
2726eleq1d 2498 . . . . 5  |-  ( g  =  F  ->  ( ran  g  e.  Fin  <->  ran  F  e.  Fin ) )
2826difeq1d 3588 . . . . . 6  |-  ( g  =  F  ->  ( ran  g  \  {  .0.  } )  =  ( ran 
F  \  {  .0.  } ) )
29 cnveq 5028 . . . . . . . . 9  |-  ( g  =  F  ->  `' g  =  `' F
)
3029imaeq1d 5187 . . . . . . . 8  |-  ( g  =  F  ->  ( `' g " {
x } )  =  ( `' F " { x } ) )
3130fveq2d 5885 . . . . . . 7  |-  ( g  =  F  ->  ( M `  ( `' g " { x }
) )  =  ( M `  ( `' F " { x } ) ) )
3231eleq1d 2498 . . . . . 6  |-  ( g  =  F  ->  (
( M `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo )  <->  ( M `  ( `' F " { x } ) )  e.  ( 0 [,) +oo ) ) )
3328, 32raleqbidv 3046 . . . . 5  |-  ( 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 ) ) )
3427, 33anbi12d 715 . . . 4  |-  ( 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 ) ) ) )
3534elrab 3235 . . 3  |-  ( F  e.  { g  e.  ( dom  MMblFnM S
)  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( M `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }  <->  ( F  e.  ( dom  MMblFnM S
)  /\  ( ran  F  e.  Fin  /\  A. x  e.  ( ran  F 
\  {  .0.  }
) ( M `  ( `' F " { x } ) )  e.  ( 0 [,) +oo ) ) ) )
3625, 35sylibr 215 . 2  |-  ( ph  ->  F  e.  { g  e.  ( dom  MMblFnM S )  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( M `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) } )
37 ovex 6333 . . 3  |-  ( W 
gsumg  ( x  e.  ( ran  F  \  {  .0.  } )  |->  ( ( H `
 ( M `  ( `' F " { x } ) ) ) 
.x.  x ) ) )  e.  _V
3837a1i 11 . 2  |-  ( ph  ->  ( W  gsumg  ( x  e.  ( ran  F  \  {  .0.  } )  |->  ( ( H `  ( M `
 ( `' F " { x } ) ) )  .x.  x
) ) )  e. 
_V )
399, 19, 36, 38fvmptd 5970 1  |-  ( ph  ->  ( ( Wsitg M
) `  F )  =  ( W  gsumg  ( x  e.  ( ran  F  \  {  .0.  } ) 
|->  ( ( H `  ( M `  ( `' F " { x } ) ) ) 
.x.  x ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1870   A.wral 2782   {crab 2786   _Vcvv 3087    \ cdif 3439   {csn 4002   U.cuni 4222    |-> cmpt 4484   `'ccnv 4853   dom cdm 4854   ran crn 4855   "cima 4857   ` cfv 5601  (class class class)co 6305   Fincfn 7577   0cc0 9538   +oocpnf 9671   [,)cico 11637   Basecbs 15084  Scalarcsca 15155   .scvsca 15156   TopOpenctopn 15279   0gc0g 15297    gsumg cgsu 15298  RRHomcrrh 28636  sigaGencsigagen 28799  measurescmeas 28856  MblFnMcmbfm 28911  sitgcsitg 28990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-sitg 28991
This theorem is referenced by:  sitgclg  29003  sitg0  29007
  Copyright terms: Public domain W3C validator