MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-itg1 Unicode version

Definition df-itg1 19501
Description: Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
df-itg1  |-  S.1  =  ( f  e.  {
g  e. MblFn  |  (
g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_
x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f " {
x } ) ) ) )
Distinct variable group:    f, g, x

Detailed syntax breakdown of Definition df-itg1
StepHypRef Expression
1 citg1 19495 . 2  class  S.1
2 vf . . 3  set  f
3 cr 8978 . . . . . 6  class  RR
4 vg . . . . . . 7  set  g
54cv 1651 . . . . . 6  class  g
63, 3, 5wf 5441 . . . . 5  wff  g : RR --> RR
75crn 4870 . . . . . 6  class  ran  g
8 cfn 7100 . . . . . 6  class  Fin
97, 8wcel 1725 . . . . 5  wff  ran  g  e.  Fin
105ccnv 4868 . . . . . . . 8  class  `' g
11 cc0 8979 . . . . . . . . . 10  class  0
1211csn 3806 . . . . . . . . 9  class  { 0 }
133, 12cdif 3309 . . . . . . . 8  class  ( RR 
\  { 0 } )
1410, 13cima 4872 . . . . . . 7  class  ( `' g " ( RR 
\  { 0 } ) )
15 cvol 19348 . . . . . . 7  class  vol
1614, 15cfv 5445 . . . . . 6  class  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )
1716, 3wcel 1725 . . . . 5  wff  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )  e.  RR
186, 9, 17w3a 936 . . . 4  wff  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR )
19 cmbf 19494 . . . 4  class MblFn
2018, 4, 19crab 2701 . . 3  class  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }
212cv 1651 . . . . . 6  class  f
2221crn 4870 . . . . 5  class  ran  f
2322, 12cdif 3309 . . . 4  class  ( ran  f  \  { 0 } )
24 vx . . . . . 6  set  x
2524cv 1651 . . . . 5  class  x
2621ccnv 4868 . . . . . . 7  class  `' f
2725csn 3806 . . . . . . 7  class  { x }
2826, 27cima 4872 . . . . . 6  class  ( `' f " { x } )
2928, 15cfv 5445 . . . . 5  class  ( vol `  ( `' f " { x } ) )
30 cmul 8984 . . . . 5  class  x.
3125, 29, 30co 6072 . . . 4  class  ( x  x.  ( vol `  ( `' f " {
x } ) ) )
3223, 31, 24csu 12467 . . 3  class  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) )
332, 20, 32cmpt 4258 . 2  class  ( f  e.  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) ) )
341, 33wceq 1652 1  wff  S.1  =  ( f  e.  {
g  e. MblFn  |  (
g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_
x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f " {
x } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  isi1f  19554  itg1val  19563
  Copyright terms: Public domain W3C validator