Theorem isi1f

Description: The predicate " F is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom F e. dom S.1 to represent this concept because S.1 is the first preparation function for our final definition S. (see df-itg ); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	isi1f	⊢ ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		feq1	⊢ ( 𝑔 = 𝐹 → ( 𝑔 : ℝ ⟶ ℝ ↔ 𝐹 : ℝ ⟶ ℝ ) )
2		rneq	⊢ ( 𝑔 = 𝐹 → ran 𝑔 = ran 𝐹 )
3	2	eleq1d	⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
4		cnveq	⊢ ( 𝑔 = 𝐹 → ◡ 𝑔 = ◡ 𝐹 )
5	4	imaeq1d	⊢ ( 𝑔 = 𝐹 → ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) = ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) )
6	5	fveq2d	⊢ ( 𝑔 = 𝐹 → ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) = ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
7	6	eleq1d	⊢ ( 𝑔 = 𝐹 → ( ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ↔ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
8	1 3 7	3anbi123d	⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ↔ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
9		sumex	⊢ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ∈ V
10		df-itg1	⊢ ∫1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) )
11	9 10	dmmpti	⊢ dom ∫1 = { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) }
12	8 11	elrab2	⊢ ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )