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

Metamath Proof Explorer

Theorem itg20

Description: The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg20 ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0

Proof

Step Hyp Ref Expression
1 i1f0 ⊢ ( ℝ × { 0 } ) ∈ dom ∫1
2 reex ⊢ ℝ ∈ V
3 2 a1i ⊢ ( ⊤ → ℝ ∈ V )
4 i1ff ⊢ ( ( ℝ × { 0 } ) ∈ dom ∫1 → ( ℝ × { 0 } ) : ℝ ⟶ ℝ )
5 1 4 mp1i ⊢ ( ⊤ → ( ℝ × { 0 } ) : ℝ ⟶ ℝ )
6 leid ⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ 𝑥 )
7 6 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ 𝑥 )
8 3 5 7 caofref ⊢ ( ⊤ → ( ℝ × { 0 } ) ∘r ≤ ( ℝ × { 0 } ) )
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 9 a1i ⊢ ( ⊤ → ℝ ⊆ ℂ )
11 5 ffnd ⊢ ( ⊤ → ( ℝ × { 0 } ) Fn ℝ )
12 10 11 0pledm ⊢ ( ⊤ → ( 0𝑝 ∘r ≤ ( ℝ × { 0 } ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( ℝ × { 0 } ) ) )
13 8 12 mpbird ⊢ ( ⊤ → 0𝑝 ∘r ≤ ( ℝ × { 0 } ) )
14 13 mptru ⊢ 0𝑝 ∘r ≤ ( ℝ × { 0 } )
15 itg2itg1 ⊢ ( ( ( ℝ × { 0 } ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( ℝ × { 0 } ) ) → ( ∫2 ‘ ( ℝ × { 0 } ) ) = ( ∫1 ‘ ( ℝ × { 0 } ) ) )
16 1 14 15 mp2an ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = ( ∫1 ‘ ( ℝ × { 0 } ) )
17 itg10 ⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0
18 16 17 eqtri ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0