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