dvmptidg

Description: Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvmptidg.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvmptidg.a	$⊢ φ \to A \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
Assertion	dvmptidg	$⊢ φ \to \frac{d (x \in A⟼ x)}{d_{S} x} = (x \in A ⟼ 1)$

Proof

Step	Hyp	Ref	Expression
1		dvmptidg.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvmptidg.a	$⊢ φ \to A \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4		sseq1	$⊢ S = ℝ \to (S \subseteq ℂ \leftrightarrow ℝ \subseteq ℂ)$
5	3 4	mpbiri	$⊢ S = ℝ \to S \subseteq ℂ$
6		eqimss	$⊢ S = ℂ \to S \subseteq ℂ$
7	5 6	pm3.2i	$⊢ ((S = ℝ \to S \subseteq ℂ) \land (S = ℂ \to S \subseteq ℂ))$
8		elpri	$⊢ S \in \{ℝ, ℂ\} \to (S = ℝ \lor S = ℂ)$
9	1 8	syl	$⊢ φ \to (S = ℝ \lor S = ℂ)$
10		pm3.44	$⊢ ((S = ℝ \to S \subseteq ℂ) \land (S = ℂ \to S \subseteq ℂ)) \to ((S = ℝ \lor S = ℂ) \to S \subseteq ℂ)$
11	7 9 10	mpsyl	$⊢ φ \to S \subseteq ℂ$
12	11	sselda	$⊢ (φ \land x \in S) \to x \in ℂ$
13		1red	$⊢ (φ \land x \in S) \to 1 \in ℝ$
14	1	dvmptid	$⊢ φ \to \frac{d (x \in S⟼ x)}{d_{S} x} = (x \in S ⟼ 1)$
15		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
16	15	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
17	16	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
18		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
19	17 11 18	syl2anc	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
20		toponss	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \land A \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to A \subseteq S$
21	19 2 20	syl2anc	$⊢ φ \to A \subseteq S$
22		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
23	1 12 13 14 21 22 15 2	dvmptres	$⊢ φ \to \frac{d (x \in A⟼ x)}{d_{S} x} = (x \in A ⟼ 1)$

Metamath Proof Explorer

Theorem dvmptidg

Proof