Theorem itg1val

Description: The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	itg1val	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )

Proof

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