Theorem dvmptidg

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

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

Proof

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