dvsconst

Description: Derivative of a constant function on the real or complex numbers. The function may return a complex A even if S is RR . (Contributed by Steve Rodriguez, 11-Nov-2015)

		Ref	Expression
	Assertion	dvsconst	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S D (S \times \{A\}) = S \times \{0\}$

Proof

Step	Hyp	Ref	Expression
1		fconst6g	$⊢ A \in ℂ \to (ℂ \times \{A\}) : ℂ ⟶ ℂ$
2	1	anim2i	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to (S \in \{ℝ, ℂ\} \land (ℂ \times \{A\}) : ℂ ⟶ ℂ)$
3		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
4		c0ex	$⊢ 0 \in V$
5	4	fconst	$⊢ (ℂ \times \{0\}) : ℂ ⟶ \{0\}$
6	5	fdmi	$⊢ dom (ℂ \times \{0\}) = ℂ$
7	3 6	sseqtrrdi	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq dom (ℂ \times \{0\})$
8	7	adantr	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S \subseteq dom (ℂ \times \{0\})$
9		dvconst	$⊢ A \in ℂ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
10	9	adantl	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
11	10	dmeqd	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to dom {(ℂ \times \{A\})}_{ℂ}^{'} = dom (ℂ \times \{0\})$
12	8 11	sseqtrrd	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'}$
13		ssid	$⊢ ℂ \subseteq ℂ$
14	12 13	jctil	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to (ℂ \subseteq ℂ \land S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'})$
15		dvres3	$⊢ ((S \in \{ℝ, ℂ\} \land (ℂ \times \{A\}) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'})) \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
16	2 14 15	syl2anc	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
17		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
18	3 17	syl	$⊢ S \in \{ℝ, ℂ\} \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
19	18	oveq2d	$⊢ S \in \{ℝ, ℂ\} \to S D ({(ℂ \times \{A\}) ↾}_{S}) = S D (S \times \{A\})$
20	19	adantr	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S D ({(ℂ \times \{A\}) ↾}_{S}) = S D (S \times \{A\})$
21	10	reseq1d	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = {(ℂ \times \{0\}) ↾}_{S}$
22		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
23	3 22	syl	$⊢ S \in \{ℝ, ℂ\} \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
24	23	adantr	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
25	21 24	eqtrd	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = S \times \{0\}$
26	16 20 25	3eqtr3d	$⊢ (S \in \{ℝ, ℂ\} \land A \in ℂ) \to S D (S \times \{A\}) = S \times \{0\}$

Metamath Proof Explorer

Theorem dvsconst

Proof