dvid

Description: Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

		Ref	Expression
	Assertion	dvid	$⊢ ℂ D ({I ↾}_{ℂ}) = ℂ \times \{1\}$

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{ℂ}) : ℂ \underset{1-1 onto}{⟶} ℂ$
2		f1of	$⊢ ({I ↾}_{ℂ}) : ℂ \underset{1-1 onto}{⟶} ℂ \to ({I ↾}_{ℂ}) : ℂ ⟶ ℂ$
3	1 2	mp1i	$⊢ ⊤ \to ({I ↾}_{ℂ}) : ℂ ⟶ ℂ$
4		simp2	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to z \in ℂ$
5		simp1	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to x \in ℂ$
6	4 5	subcld	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to z - x \in ℂ$
7		simp3	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to z \neq x$
8	4 5 7	subne0d	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to z - x \neq 0$
9		fvresi	$⊢ z \in ℂ \to ({I ↾}_{ℂ}) (z) = z$
10		fvresi	$⊢ x \in ℂ \to ({I ↾}_{ℂ}) (x) = x$
11	9 10	oveqan12rd	$⊢ (x \in ℂ \land z \in ℂ) \to ({I ↾}_{ℂ}) (z) - ({I ↾}_{ℂ}) (x) = z - x$
12	11	3adant3	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to ({I ↾}_{ℂ}) (z) - ({I ↾}_{ℂ}) (x) = z - x$
13	6 8 12	diveq1bd	$⊢ (x \in ℂ \land z \in ℂ \land z \neq x) \to \frac{({I ↾}_{ℂ}) (z) - ({I ↾}_{ℂ}) (x)}{z - x} = 1$
14	13	adantl	$⊢ (⊤ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to \frac{({I ↾}_{ℂ}) (z) - ({I ↾}_{ℂ}) (x)}{z - x} = 1$
15		ax-1cn	$⊢ 1 \in ℂ$
16	3 14 15	dvidlem	$⊢ ⊤ \to ℂ D ({I ↾}_{ℂ}) = ℂ \times \{1\}$
17	16	mptru	$⊢ ℂ D ({I ↾}_{ℂ}) = ℂ \times \{1\}$

Metamath Proof Explorer