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 ⊢ F ∈ dom ⁡ ∫ 1 → ∫ 1 ⁡ F = ∑ x ∈ ran ⁡ F ∖ 0 x ⁢ vol ⁡ F -1 x

Proof

Step Hyp Ref Expression
1 rneq ⊢ f = F → ran ⁡ f = ran ⁡ F
2 1 difeq1d ⊢ f = F → ran ⁡ f ∖ 0 = ran ⁡ F ∖ 0
3 cnveq ⊢ f = F → f -1 = F -1
4 3 imaeq1d ⊢ f = F → f -1 x = F -1 x
5 4 fveq2d ⊢ f = F → vol ⁡ f -1 x = vol ⁡ F -1 x
6 5 oveq2d ⊢ f = F → x ⁢ vol ⁡ f -1 x = x ⁢ vol ⁡ F -1 x
7 6 adantr ⊢ f = F ∧ x ∈ ran ⁡ f ∖ 0 → x ⁢ vol ⁡ f -1 x = x ⁢ vol ⁡ F -1 x
8 2 7 sumeq12dv ⊢ f = F → ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x = ∑ x ∈ ran ⁡ F ∖ 0 x ⁢ vol ⁡ F -1 x
9 df-itg1 ⊢ ∫ 1 = f ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ ⟼ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x
10 sumex ⊢ ∑ x ∈ ran ⁡ F ∖ 0 x ⁢ vol ⁡ F -1 x ∈ V
11 8 9 10 fvmpt ⊢ F ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ → ∫ 1 ⁡ F = ∑ x ∈ ran ⁡ F ∖ 0 x ⁢ vol ⁡ F -1 x
12 sumex ⊢ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x ∈ V
13 12 9 dmmpti ⊢ dom ⁡ ∫ 1 = g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ
14 11 13 eleq2s ⊢ F ∈ dom ⁡ ∫ 1 → ∫ 1 ⁡ F = ∑ x ∈ ran ⁡ F ∖ 0 x ⁢ vol ⁡ F -1 x