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

Definition df-itg1 19191
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 19185 . 2  class  S.1
2 vf . . 3  set  f
3 cr 8883 . . . . . 6  class  RR
4 vg . . . . . . 7  set  g
54cv 1646 . . . . . 6  class  g
63, 3, 5wf 5354 . . . . 5  wff  g : RR --> RR
75crn 4793 . . . . . 6  class  ran  g
8 cfn 7006 . . . . . 6  class  Fin
97, 8wcel 1715 . . . . 5  wff  ran  g  e.  Fin
105ccnv 4791 . . . . . . . 8  class  `' g
11 cc0 8884 . . . . . . . . . 10  class  0
1211csn 3729 . . . . . . . . 9  class  { 0 }
133, 12cdif 3235 . . . . . . . 8  class  ( RR 
\  { 0 } )
1410, 13cima 4795 . . . . . . 7  class  ( `' g " ( RR 
\  { 0 } ) )
15 cvol 19038 . . . . . . 7  class  vol
1614, 15cfv 5358 . . . . . 6  class  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )
1716, 3wcel 1715 . . . . 5  wff  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )  e.  RR
186, 9, 17w3a 935 . . . 4  wff  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR )
19 cmbf 19184 . . . 4  class MblFn
2018, 4, 19crab 2632 . . 3  class  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }
212cv 1646 . . . . . 6  class  f
2221crn 4793 . . . . 5  class  ran  f
2322, 12cdif 3235 . . . 4  class  ( ran  f  \  { 0 } )
24 vx . . . . . 6  set  x
2524cv 1646 . . . . 5  class  x
2621ccnv 4791 . . . . . . 7  class  `' f
2725csn 3729 . . . . . . 7  class  { x }
2826, 27cima 4795 . . . . . 6  class  ( `' f " { x } )
2928, 15cfv 5358 . . . . 5  class  ( vol `  ( `' f " { x } ) )
30 cmul 8889 . . . . 5  class  x.
3125, 29, 30co 5981 . . . 4  class  ( x  x.  ( vol `  ( `' f " {
x } ) ) )
3223, 31, 24csu 12366 . . 3  class  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) )
332, 20, 32cmpt 4179 . 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 1647 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  19244  itg1val  19253
  Copyright terms: Public domain W3C validator