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