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

Metamath Proof Explorer

Theorem itg1add

Description: The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypotheses i1fadd.1 ⊢ φ → F ∈ dom ⁡ ∫ 1
i1fadd.2 ⊢ φ → G ∈ dom ⁡ ∫ 1
Assertion itg1add ⊢ φ → ∫ 1 ⁡ F + f G = ∫ 1 ⁡ F + ∫ 1 ⁡ G

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ φ → F ∈ dom ⁡ ∫ 1
2 i1fadd.2 ⊢ φ → G ∈ dom ⁡ ∫ 1
3 eqid ⊢ i ∈ ℝ , j ∈ ℝ ⟼ if i = 0 ∧ j = 0 0 vol ⁡ F -1 i ∩ G -1 j = i ∈ ℝ , j ∈ ℝ ⟼ if i = 0 ∧ j = 0 0 vol ⁡ F -1 i ∩ G -1 j
4 eqid ⊢ + ↾ ran ⁡ F × ran ⁡ G = + ↾ ran ⁡ F × ran ⁡ G
5 1 2 3 4 itg1addlem5 ⊢ φ → ∫ 1 ⁡ F + f G = ∫ 1 ⁡ F + ∫ 1 ⁡ G