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 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) )