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	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
	i1fadd.2	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
Assertion	itg1add	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2		i1fadd.2	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3		eqid	⊢ ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ) = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
4		eqid	⊢ ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) = ( + ↾ ( ran 𝐹 × ran 𝐺 ) )
5	1 2 3 4	itg1addlem5	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) )