dvsid

Description: Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015)

		Ref	Expression
	Assertion	dvsid	$⊢ S \in \{ℝ, ℂ\} \to S D ({I ↾}_{S}) = S \times \{1\}$

Proof

Step	Hyp	Ref	Expression
1		fnresi	$⊢ ({I ↾}_{ℂ}) Fn ℂ$
2		rnresi	$⊢ ran ({I ↾}_{ℂ}) = ℂ$
3	2	eqimssi	$⊢ ran ({I ↾}_{ℂ}) \subseteq ℂ$
4		df-f	$⊢ ({I ↾}_{ℂ}) : ℂ ⟶ ℂ \leftrightarrow (({I ↾}_{ℂ}) Fn ℂ \land ran ({I ↾}_{ℂ}) \subseteq ℂ)$
5	1 3 4	mpbir2an	$⊢ ({I ↾}_{ℂ}) : ℂ ⟶ ℂ$
6	5	jctr	$⊢ S \in \{ℝ, ℂ\} \to (S \in \{ℝ, ℂ\} \land ({I ↾}_{ℂ}) : ℂ ⟶ ℂ)$
7		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
8		dvid	$⊢ ℂ D ({I ↾}_{ℂ}) = ℂ \times \{1\}$
9	8	dmeqi	$⊢ dom {({I ↾}_{ℂ})}_{ℂ}^{'} = dom (ℂ \times \{1\})$
10		1ex	$⊢ 1 \in V$
11	10	fconst	$⊢ (ℂ \times \{1\}) : ℂ ⟶ \{1\}$
12	11	fdmi	$⊢ dom (ℂ \times \{1\}) = ℂ$
13	9 12	eqtri	$⊢ dom {({I ↾}_{ℂ})}_{ℂ}^{'} = ℂ$
14	7 13	sseqtrrdi	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq dom {({I ↾}_{ℂ})}_{ℂ}^{'}$
15		ssid	$⊢ ℂ \subseteq ℂ$
16	14 15	jctil	$⊢ S \in \{ℝ, ℂ\} \to (ℂ \subseteq ℂ \land S \subseteq dom {({I ↾}_{ℂ})}_{ℂ}^{'})$
17		dvres3	$⊢ ((S \in \{ℝ, ℂ\} \land ({I ↾}_{ℂ}) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land S \subseteq dom {({I ↾}_{ℂ})}_{ℂ}^{'})) \to S D ({({I ↾}_{ℂ}) ↾}_{S}) = {{({I ↾}_{ℂ})}_{ℂ}^{'} ↾}_{S}$
18	6 16 17	syl2anc	$⊢ S \in \{ℝ, ℂ\} \to S D ({({I ↾}_{ℂ}) ↾}_{S}) = {{({I ↾}_{ℂ})}_{ℂ}^{'} ↾}_{S}$
19	7	resabs1d	$⊢ S \in \{ℝ, ℂ\} \to {({I ↾}_{ℂ}) ↾}_{S} = {I ↾}_{S}$
20	19	oveq2d	$⊢ S \in \{ℝ, ℂ\} \to S D ({({I ↾}_{ℂ}) ↾}_{S}) = S D ({I ↾}_{S})$
21	8	reseq1i	$⊢ {{({I ↾}_{ℂ})}_{ℂ}^{'} ↾}_{S} = {(ℂ \times \{1\}) ↾}_{S}$
22		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{1\}) ↾}_{S} = S \times \{1\}$
23	21 22	syl5eq	$⊢ S \subseteq ℂ \to {{({I ↾}_{ℂ})}_{ℂ}^{'} ↾}_{S} = S \times \{1\}$
24	7 23	syl	$⊢ S \in \{ℝ, ℂ\} \to {{({I ↾}_{ℂ})}_{ℂ}^{'} ↾}_{S} = S \times \{1\}$
25	18 20 24	3eqtr3d	$⊢ S \in \{ℝ, ℂ\} \to S D ({I ↾}_{S}) = S \times \{1\}$

Metamath Proof Explorer

Theorem dvsid

Proof