Metamath Proof Explorer


Definition df-itg1

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)

Ref Expression
Assertion df-itg1 1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( 𝑓 “ { 𝑥 } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 citg1 1
1 vf 𝑓
2 vg 𝑔
3 cmbf MblFn
4 2 cv 𝑔
5 cr
6 5 5 4 wf 𝑔 : ℝ ⟶ ℝ
7 4 crn ran 𝑔
8 cfn Fin
9 7 8 wcel ran 𝑔 ∈ Fin
10 cvol vol
11 4 ccnv 𝑔
12 cc0 0
13 12 csn { 0 }
14 5 13 cdif ( ℝ ∖ { 0 } )
15 11 14 cima ( 𝑔 “ ( ℝ ∖ { 0 } ) )
16 15 10 cfv ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) )
17 16 5 wcel ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ
18 6 9 17 w3a ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
19 18 2 3 crab { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) }
20 vx 𝑥
21 1 cv 𝑓
22 21 crn ran 𝑓
23 22 13 cdif ( ran 𝑓 ∖ { 0 } )
24 20 cv 𝑥
25 cmul ·
26 21 ccnv 𝑓
27 24 csn { 𝑥 }
28 26 27 cima ( 𝑓 “ { 𝑥 } )
29 28 10 cfv ( vol ‘ ( 𝑓 “ { 𝑥 } ) )
30 24 29 25 co ( 𝑥 · ( vol ‘ ( 𝑓 “ { 𝑥 } ) ) )
31 23 30 20 csu Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( 𝑓 “ { 𝑥 } ) ) )
32 1 19 31 cmpt ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( 𝑓 “ { 𝑥 } ) ) ) )
33 0 32 wceq 1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( 𝑓 “ { 𝑥 } ) ) ) )