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

Metamath Proof Explorer

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