itg10

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

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

Step	Hyp	Ref	Expression
1		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
2		itg1val	$⊢ ℝ \times \{0\} \in dom \int^{1} \to \int^{1} (ℝ \times \{0\}) = \sum_{x \in ran (ℝ \times \{0\}) ∖ \{0\}} x vol ({(ℝ \times \{0\})}^{-1} [\{x\}])$
3	1 2	ax-mp	$⊢ \int^{1} (ℝ \times \{0\}) = \sum_{x \in ran (ℝ \times \{0\}) ∖ \{0\}} x vol ({(ℝ \times \{0\})}^{-1} [\{x\}])$
4		rnxpss	$⊢ ran (ℝ \times \{0\}) \subseteq \{0\}$
5		ssdif0	$⊢ ran (ℝ \times \{0\}) \subseteq \{0\} \leftrightarrow ran (ℝ \times \{0\}) ∖ \{0\} = \emptyset$
6	4 5	mpbi	$⊢ ran (ℝ \times \{0\}) ∖ \{0\} = \emptyset$
7	6	sumeq1i	$⊢ \sum_{x \in ran (ℝ \times \{0\}) ∖ \{0\}} x vol ({(ℝ \times \{0\})}^{-1} [\{x\}]) = \sum_{x \in \emptyset} x vol ({(ℝ \times \{0\})}^{-1} [\{x\}])$
8		sum0	$⊢ \sum_{x \in \emptyset} x vol ({(ℝ \times \{0\})}^{-1} [\{x\}]) = 0$
9	3 7 8	3eqtri	$⊢ \int^{1} (ℝ \times \{0\}) = 0$

Metamath Proof Explorer