itg20

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

		Ref	Expression
	Assertion	itg20	$⊢ \int^{2} (ℝ \times \{0\}) = 0$

Step	Hyp	Ref	Expression
1		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
2		reex	$⊢ ℝ \in V$
3	2	a1i	$⊢ ⊤ \to ℝ \in V$
4		i1ff	$⊢ ℝ \times \{0\} \in dom \int^{1} \to (ℝ \times \{0\}) : ℝ ⟶ ℝ$
5	1 4	mp1i	$⊢ ⊤ \to (ℝ \times \{0\}) : ℝ ⟶ ℝ$
6		leid	$⊢ x \in ℝ \to x \leq x$
7	6	adantl	$⊢ (⊤ \land x \in ℝ) \to x \leq x$
8	3 5 7	caofref	$⊢ ⊤ \to (ℝ \times \{0\}) \leq_{f} (ℝ \times \{0\})$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10	9	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
11	5	ffnd	$⊢ ⊤ \to (ℝ \times \{0\}) Fn ℝ$
12	10 11	0pledm	$⊢ ⊤ \to (0_{𝑝} \leq_{f} (ℝ \times \{0\}) \leftrightarrow (ℝ \times \{0\}) \leq_{f} (ℝ \times \{0\}))$
13	8 12	mpbird	$⊢ ⊤ \to 0_{𝑝} \leq_{f} (ℝ \times \{0\})$
14	13	mptru	$⊢ 0_{𝑝} \leq_{f} (ℝ \times \{0\})$
15		itg2itg1	$⊢ (ℝ \times \{0\} \in dom \int^{1} \land 0_{𝑝} \leq_{f} (ℝ \times \{0\})) \to \int^{2} (ℝ \times \{0\}) = \int^{1} (ℝ \times \{0\})$
16	1 14 15	mp2an	$⊢ \int^{2} (ℝ \times \{0\}) = \int^{1} (ℝ \times \{0\})$
17		itg10	$⊢ \int^{1} (ℝ \times \{0\}) = 0$
18	16 17	eqtri	$⊢ \int^{2} (ℝ \times \{0\}) = 0$

Metamath Proof Explorer