i1f0

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

		Ref	Expression
	Assertion	i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2	1	fconst6	$⊢ (ℝ \times \{0\}) : ℝ ⟶ ℝ$
3	2	a1i	$⊢ ⊤ \to (ℝ \times \{0\}) : ℝ ⟶ ℝ$
4		snfi	$⊢ \{0\} \in Fin$
5		rnxpss	$⊢ ran (ℝ \times \{0\}) \subseteq \{0\}$
6		ssfi	$⊢ (\{0\} \in Fin \land ran (ℝ \times \{0\}) \subseteq \{0\}) \to ran (ℝ \times \{0\}) \in Fin$
7	4 5 6	mp2an	$⊢ ran (ℝ \times \{0\}) \in Fin$
8	7	a1i	$⊢ ⊤ \to ran (ℝ \times \{0\}) \in Fin$
9		difss	$⊢ ran (ℝ \times \{0\}) ∖ \{0\} \subseteq ran (ℝ \times \{0\})$
10	9 5	sstri	$⊢ ran (ℝ \times \{0\}) ∖ \{0\} \subseteq \{0\}$
11	10	sseli	$⊢ x \in (ran (ℝ \times \{0\}) ∖ \{0\}) \to x \in \{0\}$
12	11	adantl	$⊢ (⊤ \land x \in (ran (ℝ \times \{0\}) ∖ \{0\})) \to x \in \{0\}$
13		eldifn	$⊢ x \in (ran (ℝ \times \{0\}) ∖ \{0\}) \to \neg x \in \{0\}$
14	13	adantl	$⊢ (⊤ \land x \in (ran (ℝ \times \{0\}) ∖ \{0\})) \to \neg x \in \{0\}$
15	12 14	pm2.21dd	$⊢ (⊤ \land x \in (ran (ℝ \times \{0\}) ∖ \{0\})) \to {(ℝ \times \{0\})}^{-1} [\{x\}] \in dom vol$
16	12 14	pm2.21dd	$⊢ (⊤ \land x \in (ran (ℝ \times \{0\}) ∖ \{0\})) \to vol ({(ℝ \times \{0\})}^{-1} [\{x\}]) \in ℝ$
17	3 8 15 16	i1fd	$⊢ ⊤ \to ℝ \times \{0\} \in dom \int^{1}$
18	17	mptru	$⊢ ℝ \times \{0\} \in dom \int^{1}$

Metamath Proof Explorer