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

Theorem sitgval 26733
Description: Value of the simple function integral builder for a given space  W and measure  M. (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 )
Assertion
Ref Expression
sitgval  |-  ( 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 ) ) ) ) )
Distinct variable groups:    B, f    f, g, x    f, H   
f, M, g, x    S, f, g    f, W, g, x    .0. , f,
g, x    .x. , f
Allowed substitution hints:    ph( x, f, g)    B( x, g)    S( x)    .x. ( x, g)    H( x, g)    J( x, f, g)    V( x, f, g)

Proof of Theorem sitgval
Dummy variables  m  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sitgval.1 . . 3  |-  ( ph  ->  W  e.  V )
2 elex 2996 . . 3  |-  ( W  e.  V  ->  W  e.  _V )
31, 2syl 16 . 2  |-  ( ph  ->  W  e.  _V )
4 sitgval.2 . 2  |-  ( ph  ->  M  e.  U. ran measures )
5 fveq2 5706 . . . . . . . 8  |-  ( w  =  W  ->  ( TopOpen
`  w )  =  ( TopOpen `  W )
)
65fveq2d 5710 . . . . . . 7  |-  ( w  =  W  ->  (sigaGen `  ( TopOpen `  w )
)  =  (sigaGen `  ( TopOpen
`  W ) ) )
7 sitgval.s . . . . . . . 8  |-  S  =  (sigaGen `  J )
8 sitgval.j . . . . . . . . 9  |-  J  =  ( TopOpen `  W )
98fveq2i 5709 . . . . . . . 8  |-  (sigaGen `  J
)  =  (sigaGen `  ( TopOpen
`  W ) )
107, 9eqtri 2463 . . . . . . 7  |-  S  =  (sigaGen `  ( TopOpen `  W
) )
116, 10syl6eqr 2493 . . . . . 6  |-  ( w  =  W  ->  (sigaGen `  ( TopOpen `  w )
)  =  S )
1211oveq2d 6122 . . . . 5  |-  ( w  =  W  ->  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w
) ) )  =  ( dom  mMblFnM S
) )
13 fveq2 5706 . . . . . . . . . 10  |-  ( w  =  W  ->  ( 0g `  w )  =  ( 0g `  W
) )
14 sitgval.0 . . . . . . . . . 10  |-  .0.  =  ( 0g `  W )
1513, 14syl6eqr 2493 . . . . . . . . 9  |-  ( w  =  W  ->  ( 0g `  w )  =  .0.  )
1615sneqd 3904 . . . . . . . 8  |-  ( w  =  W  ->  { ( 0g `  w ) }  =  {  .0.  } )
1716difeq2d 3489 . . . . . . 7  |-  ( w  =  W  ->  ( ran  g  \  { ( 0g `  w ) } )  =  ( ran  g  \  {  .0.  } ) )
1817raleqdv 2938 . . . . . 6  |-  ( 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 ) ) )
1918anbi2d 703 . . . . 5  |-  ( 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 ) ) ) )
2012, 19rabeqbidv 2982 . . . 4  |-  ( w  =  W  ->  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w
) ) )  |  ( ran  g  e. 
Fin  /\  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }  =  { g  e.  ( dom  mMblFnM S )  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( m `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) } )
21 id 22 . . . . 5  |-  ( w  =  W  ->  w  =  W )
2216difeq2d 3489 . . . . . 6  |-  ( w  =  W  ->  ( ran  f  \  { ( 0g `  w ) } )  =  ( ran  f  \  {  .0.  } ) )
23 fveq2 5706 . . . . . . . 8  |-  ( w  =  W  ->  ( .s `  w )  =  ( .s `  W
) )
24 sitgval.x . . . . . . . 8  |-  .x.  =  ( .s `  W )
2523, 24syl6eqr 2493 . . . . . . 7  |-  ( w  =  W  ->  ( .s `  w )  = 
.x.  )
26 fveq2 5706 . . . . . . . . . 10  |-  ( w  =  W  ->  (Scalar `  w )  =  (Scalar `  W ) )
2726fveq2d 5710 . . . . . . . . 9  |-  ( w  =  W  ->  (RRHom `  (Scalar `  w )
)  =  (RRHom `  (Scalar `  W ) ) )
28 sitgval.h . . . . . . . . 9  |-  H  =  (RRHom `  (Scalar `  W
) )
2927, 28syl6eqr 2493 . . . . . . . 8  |-  ( w  =  W  ->  (RRHom `  (Scalar `  w )
)  =  H )
3029fveq1d 5708 . . . . . . 7  |-  ( w  =  W  ->  (
(RRHom `  (Scalar `  w
) ) `  (
m `  ( `' f " { x }
) ) )  =  ( H `  (
m `  ( `' f " { x }
) ) ) )
31 eqidd 2444 . . . . . . 7  |-  ( w  =  W  ->  x  =  x )
3225, 30, 31oveq123d 6127 . . . . . 6  |-  ( w  =  W  ->  (
( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x )  =  ( ( H `
 ( m `  ( `' f " {
x } ) ) )  .x.  x ) )
3322, 32mpteq12dv 4385 . . . . 5  |-  ( 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 ) ) )
3421, 33oveq12d 6124 . . . 4  |-  ( w  =  W  ->  (
w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) )  =  ( W  gsumg  ( x  e.  ( ran  f  \  {  .0.  } )  |->  ( ( H `  ( m `
 ( `' f
" { x }
) ) )  .x.  x ) ) ) )
3520, 34mpteq12dv 4385 . . 3  |-  ( w  =  W  ->  (
f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w
) ) )  |  ( ran  g  e. 
Fin  /\  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) ) )  =  ( 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 ) ) ) ) )
36 dmeq 5055 . . . . . 6  |-  ( m  =  M  ->  dom  m  =  dom  M )
3736oveq1d 6121 . . . . 5  |-  ( m  =  M  ->  ( dom  mMblFnM S )  =  ( dom  MMblFnM S
) )
38 fveq1 5705 . . . . . . . 8  |-  ( m  =  M  ->  (
m `  ( `' g " { x }
) )  =  ( M `  ( `' g " { x } ) ) )
3938eleq1d 2509 . . . . . . 7  |-  ( m  =  M  ->  (
( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo )  <->  ( M `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) )
4039ralbidv 2750 . . . . . 6  |-  ( 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 )
) )
4140anbi2d 703 . . . . 5  |-  ( 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 ) ) ) )
4237, 41rabeqbidv 2982 . . . 4  |-  ( m  =  M  ->  { g  e.  ( dom  mMblFnM S )  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }  =  { g  e.  ( dom  MMblFnM S )  |  ( ran  g  e. 
Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( M `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) } )
43 simpl 457 . . . . . . . . 9  |-  ( ( m  =  M  /\  x  e.  ( ran  f  \  {  .0.  }
) )  ->  m  =  M )
4443fveq1d 5708 . . . . . . . 8  |-  ( ( m  =  M  /\  x  e.  ( ran  f  \  {  .0.  }
) )  ->  (
m `  ( `' f " { x }
) )  =  ( M `  ( `' f " { x } ) ) )
4544fveq2d 5710 . . . . . . 7  |-  ( ( m  =  M  /\  x  e.  ( ran  f  \  {  .0.  }
) )  ->  ( H `  ( m `  ( `' f " { x } ) ) )  =  ( H `  ( M `
 ( `' f
" { x }
) ) ) )
4645oveq1d 6121 . . . . . 6  |-  ( ( m  =  M  /\  x  e.  ( ran  f  \  {  .0.  }
) )  ->  (
( H `  (
m `  ( `' f " { x }
) ) )  .x.  x )  =  ( ( H `  ( M `  ( `' f " { x }
) ) )  .x.  x ) )
4746mpteq2dva 4393 . . . . 5  |-  ( m  =  M  ->  (
x  e.  ( ran  f  \  {  .0.  } )  |->  ( ( H `
 ( m `  ( `' f " {
x } ) ) )  .x.  x ) )  =  ( x  e.  ( ran  f  \  {  .0.  } ) 
|->  ( ( H `  ( M `  ( `' f " { x } ) ) ) 
.x.  x ) ) )
4847oveq2d 6122 . . . 4  |-  ( m  =  M  ->  ( 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 ) ) ) )
4942, 48mpteq12dv 4385 . . 3  |-  ( m  =  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 ) ) ) )  =  ( 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 ) ) ) ) )
50 df-sitg 26731 . . 3  |- sitg  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w )
) )  |  ( ran  g  e.  Fin  /\ 
A. x  e.  ( ran  g  \  {
( 0g `  w
) } ) ( m `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) ) ) )
51 ovex 6131 . . . . 5  |-  ( dom 
MMblFnM S )  e.  _V
5251rabex 4458 . . . 4  |-  { g  e.  ( dom  MMblFnM S )  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  {  .0.  } ) ( M `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }  e.  _V
5352mptex 5963 . . 3  |-  ( 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 ) ) ) )  e.  _V
5435, 49, 50, 53ovmpt2 6241 . 2  |-  ( ( W  e.  _V  /\  M  e.  U. ran measures )  -> 
( 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 ) ) ) ) )
553, 4, 54syl2anc 661 1  |-  ( 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 ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2730   {crab 2734   _Vcvv 2987    \ cdif 3340   {csn 3892   U.cuni 4106    e. cmpt 4365   `'ccnv 4854   dom cdm 4855   ran crn 4856   "cima 4858   ` cfv 5433  (class class class)co 6106   Fincfn 7325   0cc0 9297   +oocpnf 9430   [,)cico 11317   Basecbs 14189  Scalarcsca 14256   .scvsca 14257   TopOpenctopn 14375   0gc0g 14393    gsumg cgsu 14394  RRHomcrrh 26437  sigaGencsigagen 26596  measurescmeas 26624  MblFnMcmbfm 26680  sitgcsitg 26730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pr 4546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-reu 2737  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-sitg 26731
This theorem is referenced by:  issibf  26734  sitgfval  26742  sitgf  26748
  Copyright terms: Public domain W3C validator