This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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