Theorem itg10

Description: The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	itg10	⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		i1f0	⊢ ( ℝ × { 0 } ) ∈ dom ∫1
2		itg1val	⊢ ( ( ℝ × { 0 } ) ∈ dom ∫1 → ( ∫1 ‘ ( ℝ × { 0 } ) ) = Σ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) ) )
3	1 2	ax-mp	⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = Σ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) )
4		rnxpss	⊢ ran ( ℝ × { 0 } ) ⊆ { 0 }
5		ssdif0	⊢ ( ran ( ℝ × { 0 } ) ⊆ { 0 } ↔ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) = ∅ )
6	4 5	mpbi	⊢ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) = ∅
7	6	sumeq1i	⊢ Σ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) ) = Σ 𝑥 ∈ ∅ ( 𝑥 · ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) )
8		sum0	⊢ Σ 𝑥 ∈ ∅ ( 𝑥 · ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) ) = 0
9	3 7 8	3eqtri	⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0