dvreslem

Description: Lemma for dvres . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Hypotheses	dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvres.t	$⊢ T = K ↾_{𝑡} S$
	dvres.g	$⊢ G = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
	dvres.s	$⊢ φ \to S \subseteq ℂ$
	dvres.f	$⊢ φ \to F : A ⟶ ℂ$
	dvres.a	$⊢ φ \to A \subseteq S$
	dvres.b	$⊢ φ \to B \subseteq S$
	dvres.y	$⊢ φ \to y \in ℂ$
Assertion	dvreslem	$⊢ φ \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y))$

Proof

Step	Hyp	Ref	Expression
1		dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
2		dvres.t	$⊢ T = K ↾_{𝑡} S$
3		dvres.g	$⊢ G = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
4		dvres.s	$⊢ φ \to S \subseteq ℂ$
5		dvres.f	$⊢ φ \to F : A ⟶ ℂ$
6		dvres.a	$⊢ φ \to A \subseteq S$
7		dvres.b	$⊢ φ \to B \subseteq S$
8		dvres.y	$⊢ φ \to y \in ℂ$
9		difss	$⊢ (A \cap B) ∖ \{x\} \subseteq A \cap B$
10		inss2	$⊢ A \cap B \subseteq B$
11	9 10	sstri	$⊢ (A \cap B) ∖ \{x\} \subseteq B$
12		simpr	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to z \in ((A \cap B) ∖ \{x\})$
13	11 12	sselid	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to z \in B$
14	13	fvresd	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to ({F ↾}_{B}) (z) = F (z)$
15	1	cnfldtop	$⊢ K \in Top$
16		cnex	$⊢ ℂ \in V$
17		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
18	4 16 17	sylancl	$⊢ φ \to S \in V$
19		resttop	$⊢ (K \in Top \land S \in V) \to K ↾_{𝑡} S \in Top$
20	15 18 19	sylancr	$⊢ φ \to K ↾_{𝑡} S \in Top$
21	2 20	eqeltrid	$⊢ φ \to T \in Top$
22		inss1	$⊢ A \cap B \subseteq A$
23	22 6	sstrid	$⊢ φ \to A \cap B \subseteq S$
24	1	cnfldtopon	$⊢ K \in TopOn (ℂ)$
25		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
26	24 4 25	sylancr	$⊢ φ \to K ↾_{𝑡} S \in TopOn (S)$
27	2 26	eqeltrid	$⊢ φ \to T \in TopOn (S)$
28		toponuni	$⊢ T \in TopOn (S) \to S = ⋃ T$
29	27 28	syl	$⊢ φ \to S = ⋃ T$
30	23 29	sseqtrd	$⊢ φ \to A \cap B \subseteq ⋃ T$
31		eqid	$⊢ ⋃ T = ⋃ T$
32	31	ntrss2	$⊢ (T \in Top \land A \cap B \subseteq ⋃ T) \to int (T) (A \cap B) \subseteq A \cap B$
33	21 30 32	syl2anc	$⊢ φ \to int (T) (A \cap B) \subseteq A \cap B$
34	33 10	sstrdi	$⊢ φ \to int (T) (A \cap B) \subseteq B$
35	34	sselda	$⊢ (φ \land x \in int (T) (A \cap B)) \to x \in B$
36	35	fvresd	$⊢ (φ \land x \in int (T) (A \cap B)) \to ({F ↾}_{B}) (x) = F (x)$
37	36	adantr	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to ({F ↾}_{B}) (x) = F (x)$
38	14 37	oveq12d	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to ({F ↾}_{B}) (z) - ({F ↾}_{B}) (x) = F (z) - F (x)$
39	38	oveq1d	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in ((A \cap B) ∖ \{x\})) \to \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x} = \frac{F (z) - F (x)}{z - x}$
40	39	mpteq2dva	$⊢ (φ \land x \in int (T) (A \cap B)) \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
41	3	reseq1i	$⊢ {G ↾}_{((A \cap B) ∖ \{x\})} = {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})}$
42		ssdif	$⊢ A \cap B \subseteq A \to (A \cap B) ∖ \{x\} \subseteq A ∖ \{x\}$
43		resmpt	$⊢ (A \cap B) ∖ \{x\} \subseteq A ∖ \{x\} \to {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
44	22 42 43	mp2b	$⊢ {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
45	41 44	eqtri	$⊢ {G ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
46	40 45	eqtr4di	$⊢ (φ \land x \in int (T) (A \cap B)) \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = {G ↾}_{((A \cap B) ∖ \{x\})}$
47	46	oveq1d	$⊢ (φ \land x \in int (T) (A \cap B)) \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x = ({G ↾}_{((A \cap B) ∖ \{x\})}) {lim}_{ℂ} x$
48	5	adantr	$⊢ (φ \land x \in int (T) (A \cap B)) \to F : A ⟶ ℂ$
49	6 4	sstrd	$⊢ φ \to A \subseteq ℂ$
50	49	adantr	$⊢ (φ \land x \in int (T) (A \cap B)) \to A \subseteq ℂ$
51	33 22	sstrdi	$⊢ φ \to int (T) (A \cap B) \subseteq A$
52	51	sselda	$⊢ (φ \land x \in int (T) (A \cap B)) \to x \in A$
53	48 50 52	dvlem	$⊢ ((φ \land x \in int (T) (A \cap B)) \land z \in (A ∖ \{x\})) \to \frac{F (z) - F (x)}{z - x} \in ℂ$
54	53 3	fmptd	$⊢ (φ \land x \in int (T) (A \cap B)) \to G : A ∖ \{x\} ⟶ ℂ$
55	22 42	mp1i	$⊢ (φ \land x \in int (T) (A \cap B)) \to (A \cap B) ∖ \{x\} \subseteq A ∖ \{x\}$
56		difss	$⊢ A ∖ \{x\} \subseteq A$
57	56 50	sstrid	$⊢ (φ \land x \in int (T) (A \cap B)) \to A ∖ \{x\} \subseteq ℂ$
58		eqid	$⊢ K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\}) = K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\})$
59		difssd	$⊢ φ \to ⋃ T ∖ A \subseteq ⋃ T$
60	30 59	unssd	$⊢ φ \to (A \cap B) \cup (⋃ T ∖ A) \subseteq ⋃ T$
61		ssun1	$⊢ A \cap B \subseteq (A \cap B) \cup (⋃ T ∖ A)$
62	61	a1i	$⊢ φ \to A \cap B \subseteq (A \cap B) \cup (⋃ T ∖ A)$
63	31	ntrss	$⊢ (T \in Top \land (A \cap B) \cup (⋃ T ∖ A) \subseteq ⋃ T \land A \cap B \subseteq (A \cap B) \cup (⋃ T ∖ A)) \to int (T) (A \cap B) \subseteq int (T) ((A \cap B) \cup (⋃ T ∖ A))$
64	21 60 62 63	syl3anc	$⊢ φ \to int (T) (A \cap B) \subseteq int (T) ((A \cap B) \cup (⋃ T ∖ A))$
65	64 51	ssind	$⊢ φ \to int (T) (A \cap B) \subseteq int (T) ((A \cap B) \cup (⋃ T ∖ A)) \cap A$
66	6 29	sseqtrd	$⊢ φ \to A \subseteq ⋃ T$
67	22	a1i	$⊢ φ \to A \cap B \subseteq A$
68		eqid	$⊢ T ↾_{𝑡} A = T ↾_{𝑡} A$
69	31 68	restntr	$⊢ (T \in Top \land A \subseteq ⋃ T \land A \cap B \subseteq A) \to int (T ↾_{𝑡} A) (A \cap B) = int (T) ((A \cap B) \cup (⋃ T ∖ A)) \cap A$
70	21 66 67 69	syl3anc	$⊢ φ \to int (T ↾_{𝑡} A) (A \cap B) = int (T) ((A \cap B) \cup (⋃ T ∖ A)) \cap A$
71	2	oveq1i	$⊢ T ↾_{𝑡} A = (K ↾_{𝑡} S) ↾_{𝑡} A$
72	15	a1i	$⊢ φ \to K \in Top$
73		restabs	$⊢ (K \in Top \land A \subseteq S \land S \in V) \to (K ↾_{𝑡} S) ↾_{𝑡} A = K ↾_{𝑡} A$
74	72 6 18 73	syl3anc	$⊢ φ \to (K ↾_{𝑡} S) ↾_{𝑡} A = K ↾_{𝑡} A$
75	71 74	eqtrid	$⊢ φ \to T ↾_{𝑡} A = K ↾_{𝑡} A$
76	75	fveq2d	$⊢ φ \to int (T ↾_{𝑡} A) = int (K ↾_{𝑡} A)$
77	76	fveq1d	$⊢ φ \to int (T ↾_{𝑡} A) (A \cap B) = int (K ↾_{𝑡} A) (A \cap B)$
78	70 77	eqtr3d	$⊢ φ \to int (T) ((A \cap B) \cup (⋃ T ∖ A)) \cap A = int (K ↾_{𝑡} A) (A \cap B)$
79	65 78	sseqtrd	$⊢ φ \to int (T) (A \cap B) \subseteq int (K ↾_{𝑡} A) (A \cap B)$
80	79	sselda	$⊢ (φ \land x \in int (T) (A \cap B)) \to x \in int (K ↾_{𝑡} A) (A \cap B)$
81		undif1	$⊢ (A ∖ \{x\}) \cup \{x\} = A \cup \{x\}$
82	33	sselda	$⊢ (φ \land x \in int (T) (A \cap B)) \to x \in (A \cap B)$
83	82	snssd	$⊢ (φ \land x \in int (T) (A \cap B)) \to \{x\} \subseteq A \cap B$
84	83 22	sstrdi	$⊢ (φ \land x \in int (T) (A \cap B)) \to \{x\} \subseteq A$
85		ssequn2	$⊢ \{x\} \subseteq A \leftrightarrow A \cup \{x\} = A$
86	84 85	sylib	$⊢ (φ \land x \in int (T) (A \cap B)) \to A \cup \{x\} = A$
87	81 86	eqtrid	$⊢ (φ \land x \in int (T) (A \cap B)) \to (A ∖ \{x\}) \cup \{x\} = A$
88	87	oveq2d	$⊢ (φ \land x \in int (T) (A \cap B)) \to K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\}) = K ↾_{𝑡} A$
89	88	fveq2d	$⊢ (φ \land x \in int (T) (A \cap B)) \to int (K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\})) = int (K ↾_{𝑡} A)$
90		undif1	$⊢ ((A \cap B) ∖ \{x\}) \cup \{x\} = (A \cap B) \cup \{x\}$
91		ssequn2	$⊢ \{x\} \subseteq A \cap B \leftrightarrow (A \cap B) \cup \{x\} = A \cap B$
92	83 91	sylib	$⊢ (φ \land x \in int (T) (A \cap B)) \to (A \cap B) \cup \{x\} = A \cap B$
93	90 92	eqtrid	$⊢ (φ \land x \in int (T) (A \cap B)) \to ((A \cap B) ∖ \{x\}) \cup \{x\} = A \cap B$
94	89 93	fveq12d	$⊢ (φ \land x \in int (T) (A \cap B)) \to int (K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\})) (((A \cap B) ∖ \{x\}) \cup \{x\}) = int (K ↾_{𝑡} A) (A \cap B)$
95	80 94	eleqtrrd	$⊢ (φ \land x \in int (T) (A \cap B)) \to x \in int (K ↾_{𝑡} ((A ∖ \{x\}) \cup \{x\})) (((A \cap B) ∖ \{x\}) \cup \{x\})$
96	54 55 57 1 58 95	limcres	$⊢ (φ \land x \in int (T) (A \cap B)) \to ({G ↾}_{((A \cap B) ∖ \{x\})}) {lim}_{ℂ} x = G {lim}_{ℂ} x$
97	47 96	eqtrd	$⊢ (φ \land x \in int (T) (A \cap B)) \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x = G {lim}_{ℂ} x$
98	97	eleq2d	$⊢ (φ \land x \in int (T) (A \cap B)) \to (y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x) \leftrightarrow y \in (G {lim}_{ℂ} x))$
99	98	pm5.32da	$⊢ φ \to ((x \in int (T) (A \cap B) \land y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)) \leftrightarrow (x \in int (T) (A \cap B) \land y \in (G {lim}_{ℂ} x)))$
100	7 29	sseqtrd	$⊢ φ \to B \subseteq ⋃ T$
101	31	ntrin	$⊢ (T \in Top \land A \subseteq ⋃ T \land B \subseteq ⋃ T) \to int (T) (A \cap B) = int (T) (A) \cap int (T) (B)$
102	21 66 100 101	syl3anc	$⊢ φ \to int (T) (A \cap B) = int (T) (A) \cap int (T) (B)$
103	102	eleq2d	$⊢ φ \to (x \in int (T) (A \cap B) \leftrightarrow x \in (int (T) (A) \cap int (T) (B)))$
104		elin	$⊢ x \in (int (T) (A) \cap int (T) (B)) \leftrightarrow (x \in int (T) (A) \land x \in int (T) (B))$
105	103 104	bitrdi	$⊢ φ \to (x \in int (T) (A \cap B) \leftrightarrow (x \in int (T) (A) \land x \in int (T) (B)))$
106	105	anbi1d	$⊢ φ \to ((x \in int (T) (A \cap B) \land y \in (G {lim}_{ℂ} x)) \leftrightarrow ((x \in int (T) (A) \land x \in int (T) (B)) \land y \in (G {lim}_{ℂ} x)))$
107	99 106	bitrd	$⊢ φ \to ((x \in int (T) (A \cap B) \land y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)) \leftrightarrow ((x \in int (T) (A) \land x \in int (T) (B)) \land y \in (G {lim}_{ℂ} x)))$
108		an32	$⊢ ((x \in int (T) (A) \land x \in int (T) (B)) \land y \in (G {lim}_{ℂ} x)) \leftrightarrow ((x \in int (T) (A) \land y \in (G {lim}_{ℂ} x)) \land x \in int (T) (B))$
109	107 108	bitrdi	$⊢ φ \to ((x \in int (T) (A \cap B) \land y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)) \leftrightarrow ((x \in int (T) (A) \land y \in (G {lim}_{ℂ} x)) \land x \in int (T) (B)))$
110		eqid	$⊢ (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x})$
111		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{B}) : A \cap B ⟶ ℂ$
112	5 111	syl	$⊢ φ \to ({F ↾}_{B}) : A \cap B ⟶ ℂ$
113	2 1 110 4 112 23	eldv	$⊢ φ \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (A \cap B) \land y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)))$
114	2 1 3 4 5 6	eldv	$⊢ φ \to (x F_{S}^{'} y \leftrightarrow (x \in int (T) (A) \land y \in (G {lim}_{ℂ} x)))$
115	114	anbi1cd	$⊢ φ \to ((x \in int (T) (B) \land x F_{S}^{'} y) \leftrightarrow ((x \in int (T) (A) \land y \in (G {lim}_{ℂ} x)) \land x \in int (T) (B)))$
116	109 113 115	3bitr4d	$⊢ φ \to (x {({F ↾}_{B})}_{S}^{'} y \leftrightarrow (x \in int (T) (B) \land x F_{S}^{'} y))$

Metamath Proof Explorer

Theorem dvreslem

Proof