Theorem dvres2lem

Description: Lemma for dvres2 . (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	dvres.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvres.t	$$⊢T=K{\upharpoonright }_{𝑡}S$$
	dvres.g	$$⊢G=\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
	dvres.s	$$⊢\phi \to S\subseteq ℂ$$
	dvres.f	$$⊢\phi \to F:A⟶ℂ$$
	dvres.a	$$⊢\phi \to A\subseteq S$$
	dvres.b	$$⊢\phi \to B\subseteq S$$
	dvres.y	$$⊢\phi \to y\in ℂ$$
	dvres2lem.d	$$⊢\phi \to x{F}_S^{\prime }y$$
	dvres2lem.x	$$⊢\phi \to x\in B$$
Assertion	dvres2lem	$$⊢\phi \to x{\left({F\upharpoonright }_B\right)}_B^{\prime }y$$

Proof

Step	Hyp	Ref	Expression
1		dvres.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		dvres.t	$$⊢T=K{\upharpoonright }_{𝑡}S$$
3		dvres.g	$$⊢G=\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
4		dvres.s	$$⊢\phi \to S\subseteq ℂ$$
5		dvres.f	$$⊢\phi \to F:A⟶ℂ$$
6		dvres.a	$$⊢\phi \to A\subseteq S$$
7		dvres.b	$$⊢\phi \to B\subseteq S$$
8		dvres.y	$$⊢\phi \to y\in ℂ$$
9		dvres2lem.d	$$⊢\phi \to x{F}_S^{\prime }y$$
10		dvres2lem.x	$$⊢\phi \to x\in B$$
11	1	cnfldtop	$$⊢K\in \mathrm{Top}$$
12		cnex	$$⊢ℂ\in \mathrm{V}$$
13		ssexg	$$⊢\left(S\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to S\in \mathrm{V}$$
14	4 12 13	sylancl	$$⊢\phi \to S\in \mathrm{V}$$
15		resttop	$$⊢\left(K\in \mathrm{Top}\wedge S\in \mathrm{V}\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
16	11 14 15	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
17	2 16	eqeltrid	$$⊢\phi \to T\in \mathrm{Top}$$
18		inss1	$$⊢A\cap B\subseteq A$$
19	18 6	sstrid	$$⊢\phi \to A\cap B\subseteq S$$
20	1	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
21		resttopon	$$⊢\left(K\in \mathrm{TopOn}\left(ℂ\right)\wedge S\subseteq ℂ\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
22	20 4 21	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
23	2 22	eqeltrid	$$⊢\phi \to T\in \mathrm{TopOn}\left(S\right)$$
24		toponuni	$$⊢T\in \mathrm{TopOn}\left(S\right)\to S=\bigcup T$$
25	23 24	syl	$$⊢\phi \to S=\bigcup T$$
26	19 25	sseqtrd	$$⊢\phi \to A\cap B\subseteq \bigcup T$$
27		difssd	$$⊢\phi \to \bigcup T\setminus B\subseteq \bigcup T$$
28	26 27	unssd	$$⊢\phi \to \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\subseteq \bigcup T$$
29		inundif	$$⊢\left(A\cap B\right)\cup \left(A\setminus B\right)=A$$
30	6 25	sseqtrd	$$⊢\phi \to A\subseteq \bigcup T$$
31		ssdif	$$⊢A\subseteq \bigcup T\to A\setminus B\subseteq \bigcup T\setminus B$$
32		unss2	$$⊢A\setminus B\subseteq \bigcup T\setminus B\to \left(A\cap B\right)\cup \left(A\setminus B\right)\subseteq \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)$$
33	30 31 32	3syl	$$⊢\phi \to \left(A\cap B\right)\cup \left(A\setminus B\right)\subseteq \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)$$
34	29 33	eqsstrrid	$$⊢\phi \to A\subseteq \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)$$
35		eqid	$$⊢\bigcup T=\bigcup T$$
36	35	ntrss	$$⊢\left(T\in \mathrm{Top}\wedge \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\subseteq \bigcup T\wedge A\subseteq \left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)\to \mathrm{int}\left(T\right)\left(A\right)\subseteq \mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)$$
37	17 28 34 36	syl3anc	$$⊢\phi \to \mathrm{int}\left(T\right)\left(A\right)\subseteq \mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)$$
38	2 1 3 4 5 6	eldv	$$⊢\phi \to \left(x{F}_S^{\prime }y\leftrightarrow \left(x\in \mathrm{int}\left(T\right)\left(A\right)\wedge y\in \left(G{lim}_{ℂ}x\right)\right)\right)$$
39	9 38	mpbid	$$⊢\phi \to \left(x\in \mathrm{int}\left(T\right)\left(A\right)\wedge y\in \left(G{lim}_{ℂ}x\right)\right)$$
40	39	simpld	$$⊢\phi \to x\in \mathrm{int}\left(T\right)\left(A\right)$$
41	37 40	sseldd	$$⊢\phi \to x\in \mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)$$
42	41 10	elind	$$⊢\phi \to x\in \left(\mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)\cap B\right)$$
43	7 25	sseqtrd	$$⊢\phi \to B\subseteq \bigcup T$$
44		inss2	$$⊢A\cap B\subseteq B$$
45	44	a1i	$$⊢\phi \to A\cap B\subseteq B$$
46		eqid	$$⊢T{\upharpoonright }_{𝑡}B=T{\upharpoonright }_{𝑡}B$$
47	35 46	restntr	$$⊢\left(T\in \mathrm{Top}\wedge B\subseteq \bigcup T\wedge A\cap B\subseteq B\right)\to \mathrm{int}\left(T{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)=\mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)\cap B$$
48	17 43 45 47	syl3anc	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)=\mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)\cap B$$
49	2	oveq1i	$$⊢T{\upharpoonright }_{𝑡}B=\left(K{\upharpoonright }_{𝑡}S\right){\upharpoonright }_{𝑡}B$$
50	11	a1i	$$⊢\phi \to K\in \mathrm{Top}$$
51		restabs	$$⊢\left(K\in \mathrm{Top}\wedge B\subseteq S\wedge S\in \mathrm{V}\right)\to \left(K{\upharpoonright }_{𝑡}S\right){\upharpoonright }_{𝑡}B=K{\upharpoonright }_{𝑡}B$$
52	50 7 14 51	syl3anc	$$⊢\phi \to \left(K{\upharpoonright }_{𝑡}S\right){\upharpoonright }_{𝑡}B=K{\upharpoonright }_{𝑡}B$$
53	49 52	syl5eq	$$⊢\phi \to T{\upharpoonright }_{𝑡}B=K{\upharpoonright }_{𝑡}B$$
54	53	fveq2d	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}B\right)=\mathrm{int}\left(K{\upharpoonright }_{𝑡}B\right)$$
55	54	fveq1d	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)=\mathrm{int}\left(K{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)$$
56	48 55	eqtr3d	$$⊢\phi \to \mathrm{int}\left(T\right)\left(\left(A\cap B\right)\cup \left(\bigcup T\setminus B\right)\right)\cap B=\mathrm{int}\left(K{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)$$
57	42 56	eleqtrd	$$⊢\phi \to x\in \mathrm{int}\left(K{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)$$
58		limcresi	$$⊢G{lim}_{ℂ}x\subseteq \left({G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x$$
59	39	simprd	$$⊢\phi \to y\in \left(G{lim}_{ℂ}x\right)$$
60	58 59	sseldi	$$⊢\phi \to y\in \left(\left({G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x\right)$$
61		difss	$$⊢\left(A\cap B\right)\setminus \left\{x\right\}\subseteq A\cap B$$
62	61 44	sstri	$$⊢\left(A\cap B\right)\setminus \left\{x\right\}\subseteq B$$
63	62	sseli	$$⊢z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)\to z\in B$$
64		fvres	$$⊢z\in B\to \left({F\upharpoonright }_B\right)\left(z\right)=F\left(z\right)$$
65	10	fvresd	$$⊢\phi \to \left({F\upharpoonright }_B\right)\left(x\right)=F\left(x\right)$$
66	64 65	oveqan12rd	$$⊢\left(\phi \wedge z\in B\right)\to \left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)=F\left(z\right)-F\left(x\right)$$
67	66	oveq1d	$$⊢\left(\phi \wedge z\in B\right)\to \frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}=\frac{F\left(z\right)-F\left(x\right)}{z-x}$$
68	63 67	sylan2	$$⊢\left(\phi \wedge z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)\right)\to \frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}=\frac{F\left(z\right)-F\left(x\right)}{z-x}$$
69	68	mpteq2dva	$$⊢\phi \to \left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right)=\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
70	3	reseq1i	$$⊢{G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}={\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}$$
71		ssdif	$$⊢A\cap B\subseteq A\to \left(A\cap B\right)\setminus \left\{x\right\}\subseteq A\setminus \left\{x\right\}$$
72		resmpt	$$⊢\left(A\cap B\right)\setminus \left\{x\right\}\subseteq A\setminus \left\{x\right\}\to {\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}=\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
73	18 71 72	mp2b	$$⊢{\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}=\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
74	70 73	eqtri	$$⊢{G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}=\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
75	69 74	eqtr4di	$$⊢\phi \to \left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right)={G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}$$
76	75	oveq1d	$$⊢\phi \to \left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right){lim}_{ℂ}x=\left({G\upharpoonright }_{\left(\left(A\cap B\right)\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x$$
77	60 76	eleqtrrd	$$⊢\phi \to y\in \left(\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)$$
78		eqid	$$⊢K{\upharpoonright }_{𝑡}B=K{\upharpoonright }_{𝑡}B$$
79		eqid	$$⊢\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right)=\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right)$$
80	7 4	sstrd	$$⊢\phi \to B\subseteq ℂ$$
81		fresin	$$⊢F:A⟶ℂ\to \left({F\upharpoonright }_B\right):A\cap B⟶ℂ$$
82	5 81	syl	$$⊢\phi \to \left({F\upharpoonright }_B\right):A\cap B⟶ℂ$$
83	78 1 79 80 82 45	eldv	$$⊢\phi \to \left(x{\left({F\upharpoonright }_B\right)}_B^{\prime }y\leftrightarrow \left(x\in \mathrm{int}\left(K{\upharpoonright }_{𝑡}B\right)\left(A\cap B\right)\wedge y\in \left(\left(z\in \left(\left(A\cap B\right)\setminus \left\{x\right\}\right)⟼\frac{\left({F\upharpoonright }_B\right)\left(z\right)-\left({F\upharpoonright }_B\right)\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\right)$$
84	57 77 83	mpbir2and	$$⊢\phi \to x{\left({F\upharpoonright }_B\right)}_B^{\prime }y$$