dvcnvlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvcnvlem		Structured version Visualization version GIF version

Theorem dvcnvlem 26351

Description: Lemma for dvcnvre 26394. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)

**Hypotheses**
Ref	Expression
dvcnv.j	⊢ 𝐽 = (TopOpen‘ℂ_fld)
dvcnv.k	⊢ 𝐾 = (𝐽 ↾_t 𝑆)
dvcnv.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
dvcnv.y	⊢ (𝜑 → 𝑌 ∈ 𝐾)
dvcnv.f	⊢ (𝜑 → 𝐹:𝑋⟶1-1onto𝑌)
dvcnv.i	⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
dvcnv.d	⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
dvcnv.z	⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))
dvcnv.c	⊢ (𝜑 → 𝐶 ∈ 𝑋)

**Assertion**
Ref	Expression
dvcnvlem	⊢ (𝜑 → (𝐹‘𝐶)(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘𝐶)))

Proof of Theorem dvcnvlem Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvcnv.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶1-1onto𝑌)
2		f1of 6854	. . . . 5 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → 𝐹:𝑋⟶𝑌)
3	1, 2	syl 18	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
4		dvcnv.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
5	3, 4	ffvelcdmd 7117	. . 3 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝑌)
6		dvcnv.k	. . . . . 6 ⊢ 𝐾 = (𝐽 ↾_t 𝑆)
7		dvcnv.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
8	7	cnfldtopon 25156	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
9		dvcnv.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
10		recnprss 26279	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
11	9, 10	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		resttopon 23534	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
13	8, 11, 12	sylancr 599	. . . . . 6 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
14	6, 13	eqeltrid 2868	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑆))
15		topontop 23286	. . . . 5 ⊢ (𝐾 ∈ (TopOn‘𝑆) → 𝐾 ∈ Top)
16	14, 15	syl 18	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Top)
17		dvcnv.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
18		isopn3i 23455	. . . 4 ⊢ ((𝐾 ∈ Top ∧ 𝑌 ∈ 𝐾) → ((int‘𝐾)‘𝑌) = 𝑌)
19	16, 17, 18	syl2anc 596	. . 3 ⊢ (𝜑 → ((int‘𝐾)‘𝑌) = 𝑌)
20	5, 19	eleqtrrd 2867	. 2 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝐾)‘𝑌))
21		f1ocnv 6867	. . . . . . . . 9 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → ^◡𝐹:𝑌⟶1-1onto𝑋)
22		f1of 6854	. . . . . . . . 9 ⊢ (^◡𝐹:𝑌⟶1-1onto𝑋 → ^◡𝐹:𝑌⟶𝑋)
23	1, 21, 22	3syl 19	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
24		eldifi 4070	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) → 𝑧 ∈ 𝑌)
25		ffvelcdm 7113	. . . . . . . 8 ⊢ ((^◡𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → (^◡𝐹‘𝑧) ∈ 𝑋)
26	23, 24, 25	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → (^◡𝐹‘𝑧) ∈ 𝑋)
27	26	anim1i 627	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) ∧ (^◡𝐹‘𝑧) ≠ 𝐶) → ((^◡𝐹‘𝑧) ∈ 𝑋 ∧ (^◡𝐹‘𝑧) ≠ 𝐶))
28		eldifsn 4750	. . . . . 6 ⊢ ((^◡𝐹‘𝑧) ∈ (𝑋 ∖ {𝐶}) ↔ ((^◡𝐹‘𝑧) ∈ 𝑋 ∧ (^◡𝐹‘𝑧) ≠ 𝐶))
29	27, 28	sylibr 237	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) ∧ (^◡𝐹‘𝑧) ≠ 𝐶) → (^◡𝐹‘𝑧) ∈ (𝑋 ∖ {𝐶}))
30	29	anasss 472	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ∧ (^◡𝐹‘𝑧) ≠ 𝐶)) → (^◡𝐹‘𝑧) ∈ (𝑋 ∖ {𝐶}))
31		eldifi 4070	. . . . . . 7 ⊢ (𝑦 ∈ (𝑋 ∖ {𝐶}) → 𝑦 ∈ 𝑋)
32		dvcnv.d	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
33		dvbsss 26277	. . . . . . . . . 10 ⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
34	32, 33	eqsstrrdi 3958	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
35	34, 11	sstrd 3923	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
36	35	sselda 3913	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ)
37	31, 36	sylan2 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝑦 ∈ ℂ)
38	34, 4	sseldd 3914	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
39	11, 38	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
40	39	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ)
41	37, 40	subcld 11708	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (𝑦 − 𝐶) ∈ ℂ)
42		toponss 23300	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (TopOn‘𝑆) ∧ 𝑌 ∈ 𝐾) → 𝑌 ⊆ 𝑆)
43	14, 17, 42	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
44	43, 11	sstrd 3923	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
45	3, 44	fssd 6757	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
46		ffvelcdm 7113	. . . . . . 7 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ℂ)
47	45, 31, 46	syl2an 608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝑦) ∈ ℂ)
48	44, 5	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
49	48	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
50	47, 49	subcld 11708	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑦) − (𝐹‘𝐶)) ∈ ℂ)
51		eldifsni 4755	. . . . . . 7 ⊢ (𝑦 ∈ (𝑋 ∖ {𝐶}) → 𝑦 ≠ 𝐶)
52	51	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝑦 ≠ 𝐶)
53	47, 49	subeq0ad 11716	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) = 0 ↔ (𝐹‘𝑦) = (𝐹‘𝐶)))
54		f1of1 6853	. . . . . . . . . . 11 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → 𝐹:𝑋⟶1-1𝑌)
55	1, 54	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝑋⟶1-1𝑌)
56	55	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶1-1𝑌)
57	31	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝑦 ∈ 𝑋)
58	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ 𝑋)
59		f1fveq 7297	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶1-1𝑌 ∧ (𝑦 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐹‘𝑦) = (𝐹‘𝐶) ↔ 𝑦 = 𝐶))
60	56, 57, 58, 59	syl12anc 850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑦) = (𝐹‘𝐶) ↔ 𝑦 = 𝐶))
61	53, 60	bitrd 282	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) = 0 ↔ 𝑦 = 𝐶))
62	61	necon3bid 3003	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) ≠ 0 ↔ 𝑦 ≠ 𝐶))
63	52, 62	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑦) − (𝐹‘𝐶)) ≠ 0)
64	41, 50, 63	divcld 12133	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶))) ∈ ℂ)
65		limcresi 26260	. . . . . 6 ⊢ (^◡𝐹 lim_ℂ (𝐹‘𝐶)) ⊆ ((^◡𝐹 ↾ (𝑌 ∖ {(𝐹‘𝐶)})) lim_ℂ (𝐹‘𝐶))
66	23	feqmptd 6984	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝑌 ↦ (^◡𝐹‘𝑧)))
67	66	reseq1d 5985	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐹 ↾ (𝑌 ∖ {(𝐹‘𝐶)})) = ((𝑧 ∈ 𝑌 ↦ (^◡𝐹‘𝑧)) ↾ (𝑌 ∖ {(𝐹‘𝐶)})))
68		difss 4075	. . . . . . . . 9 ⊢ (𝑌 ∖ {(𝐹‘𝐶)}) ⊆ 𝑌
69		resmpt 6047	. . . . . . . . 9 ⊢ ((𝑌 ∖ {(𝐹‘𝐶)}) ⊆ 𝑌 → ((𝑧 ∈ 𝑌 ↦ (^◡𝐹‘𝑧)) ↾ (𝑌 ∖ {(𝐹‘𝐶)})) = (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧)))
70	68, 69	ax-mp 5	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑌 ↦ (^◡𝐹‘𝑧)) ↾ (𝑌 ∖ {(𝐹‘𝐶)})) = (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧))
71	67, 70	eqtrdi 2814	. . . . . . 7 ⊢ (𝜑 → (^◡𝐹 ↾ (𝑌 ∖ {(𝐹‘𝐶)})) = (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧)))
72	71	oveq1d 7466	. . . . . 6 ⊢ (𝜑 → ((^◡𝐹 ↾ (𝑌 ∖ {(𝐹‘𝐶)})) lim_ℂ (𝐹‘𝐶)) = ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧)) lim_ℂ (𝐹‘𝐶)))
73	65, 72	sseqtrid 3955	. . . . 5 ⊢ (𝜑 → (^◡𝐹 lim_ℂ (𝐹‘𝐶)) ⊆ ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧)) lim_ℂ (𝐹‘𝐶)))
74		f1ocnvfv1 7315	. . . . . . 7 ⊢ ((𝐹:𝑋⟶1-1onto𝑌 ∧ 𝐶 ∈ 𝑋) → (^◡𝐹‘(𝐹‘𝐶)) = 𝐶)
75	1, 4, 74	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (^◡𝐹‘(𝐹‘𝐶)) = 𝐶)
76		dvcnv.i	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
77	76, 5	cnlimci 26264	. . . . . 6 ⊢ (𝜑 → (^◡𝐹‘(𝐹‘𝐶)) ∈ (^◡𝐹 lim_ℂ (𝐹‘𝐶)))
78	75, 77	eqeltrrd 2865	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (^◡𝐹 lim_ℂ (𝐹‘𝐶)))
79	73, 78	sseldd 3914	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (^◡𝐹‘𝑧)) lim_ℂ (𝐹‘𝐶)))
80	45, 35, 4	dvlem 26271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ∈ ℂ)
81	37, 40, 52	subne0d 11718	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (𝑦 − 𝐶) ≠ 0)
82	50, 41, 63, 81	divne0d 12149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ≠ 0)
83		eldifsn 4750	. . . . . . . 8 ⊢ ((((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ∈ (ℂ ∖ {0}) ↔ ((((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ∈ ℂ ∧ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ≠ 0))
84	80, 82, 83	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) ∈ (ℂ ∖ {0}))
85	84	fmpttd 7147	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))):(𝑋 ∖ {𝐶})⟶(ℂ ∖ {0}))
86		difss 4075	. . . . . . 7 ⊢ (ℂ ∖ {0}) ⊆ ℂ
87	86	a1i 11	. . . . . 6 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
88		eqid 2763	. . . . . 6 ⊢ (𝐽 ↾_t (ℂ ∖ {0})) = (𝐽 ↾_t (ℂ ∖ {0}))
89	4, 32	eleqtrrd 2867	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
90		dvfg 26281	. . . . . . . . . 10 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
91		ffun 6742	. . . . . . . . . 10 ⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ → Fun (𝑆 D 𝐹))
92		funfvbrb 7081	. . . . . . . . . 10 ⊢ (Fun (𝑆 D 𝐹) → (𝐶 ∈ dom (𝑆 D 𝐹) ↔ 𝐶(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝐶)))
93	9, 90, 91, 92	4syl 20	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 ∈ dom (𝑆 D 𝐹) ↔ 𝐶(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝐶)))
94	89, 93	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝐶))
95		eqid 2763	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) = (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))
96	6, 7, 95, 11, 45, 34	eldv 26273	. . . . . . . 8 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘𝐾)‘𝑋) ∧ ((𝑆 D 𝐹)‘𝐶) ∈ ((𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) lim_ℂ 𝐶))))
97	94, 96	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ ((int‘𝐾)‘𝑋) ∧ ((𝑆 D 𝐹)‘𝐶) ∈ ((𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) lim_ℂ 𝐶)))
98	97	simprd 501	. . . . . 6 ⊢ (𝜑 → ((𝑆 D 𝐹)‘𝐶) ∈ ((𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) lim_ℂ 𝐶))
99		resttopon 23534	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾_t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
100	8, 86, 99	mp2an 705	. . . . . . . . 9 ⊢ (𝐽 ↾_t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
101	100	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐽 ↾_t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
102	8	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘ℂ))
103		1cnd 11341	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
104	101, 102, 103	cnmptc 24036	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ 1) ∈ ((𝐽 ↾_t (ℂ ∖ {0})) Cn 𝐽))
105	101	cnmptid 24035	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ 𝑥) ∈ ((𝐽 ↾_t (ℂ ∖ {0})) Cn (𝐽 ↾_t (ℂ ∖ {0}))))
106	7, 88	divcn 25244	. . . . . . . . 9 ⊢ / ∈ ((𝐽 ×_t (𝐽 ↾_t (ℂ ∖ {0}))) Cn 𝐽)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → / ∈ ((𝐽 ×_t (𝐽 ↾_t (ℂ ∖ {0}))) Cn 𝐽))
108	101, 104, 105, 107	cnmpt12f 24040	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((𝐽 ↾_t (ℂ ∖ {0})) Cn 𝐽))
109	9, 90	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
110	32	feq2d 6723	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ))
111	109, 110	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ)
112	111, 4	ffvelcdmd 7117	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D 𝐹)‘𝐶) ∈ ℂ)
113	109	ffnd 6740	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D 𝐹) Fn dom (𝑆 D 𝐹))
114		fnfvelrn 7112	. . . . . . . . . 10 ⊢ (((𝑆 D 𝐹) Fn dom (𝑆 D 𝐹) ∧ 𝐶 ∈ dom (𝑆 D 𝐹)) → ((𝑆 D 𝐹)‘𝐶) ∈ ran (𝑆 D 𝐹))
115	113, 89, 114	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D 𝐹)‘𝐶) ∈ ran (𝑆 D 𝐹))
116		dvcnv.z	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))
117		nelne2 3057	. . . . . . . . 9 ⊢ ((((𝑆 D 𝐹)‘𝐶) ∈ ran (𝑆 D 𝐹) ∧ ¬ 0 ∈ ran (𝑆 D 𝐹)) → ((𝑆 D 𝐹)‘𝐶) ≠ 0)
118	115, 116, 117	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D 𝐹)‘𝐶) ≠ 0)
119		eldifsn 4750	. . . . . . . 8 ⊢ (((𝑆 D 𝐹)‘𝐶) ∈ (ℂ ∖ {0}) ↔ (((𝑆 D 𝐹)‘𝐶) ∈ ℂ ∧ ((𝑆 D 𝐹)‘𝐶) ≠ 0))
120	112, 118, 119	sylanbrc 595	. . . . . . 7 ⊢ (𝜑 → ((𝑆 D 𝐹)‘𝐶) ∈ (ℂ ∖ {0}))
121	100	toponunii 23289	. . . . . . . 8 ⊢ (ℂ ∖ {0}) = ∪ (𝐽 ↾_t (ℂ ∖ {0}))
122	121	cncnpi 23651	. . . . . . 7 ⊢ (((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((𝐽 ↾_t (ℂ ∖ {0})) Cn 𝐽) ∧ ((𝑆 D 𝐹)‘𝐶) ∈ (ℂ ∖ {0})) → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ (((𝐽 ↾_t (ℂ ∖ {0})) CnP 𝐽)‘((𝑆 D 𝐹)‘𝐶)))
123	108, 120, 122	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ (((𝐽 ↾_t (ℂ ∖ {0})) CnP 𝐽)‘((𝑆 D 𝐹)‘𝐶)))
124	85, 87, 7, 88, 98, 123	limccnp 26266	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))‘((𝑆 D 𝐹)‘𝐶)) ∈ (((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))) lim_ℂ 𝐶))
125		oveq2 7459	. . . . . . 7 ⊢ (𝑥 = ((𝑆 D 𝐹)‘𝐶) → (1 / 𝑥) = (1 / ((𝑆 D 𝐹)‘𝐶)))
126		eqid 2763	. . . . . . 7 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
127		ovex 7484	. . . . . . 7 ⊢ (1 / ((𝑆 D 𝐹)‘𝐶)) ∈ V
128	125, 126, 127	fvmpt 7024	. . . . . 6 ⊢ (((𝑆 D 𝐹)‘𝐶) ∈ (ℂ ∖ {0}) → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))‘((𝑆 D 𝐹)‘𝐶)) = (1 / ((𝑆 D 𝐹)‘𝐶)))
129	120, 128	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))‘((𝑆 D 𝐹)‘𝐶)) = (1 / ((𝑆 D 𝐹)‘𝐶)))
130		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) = (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))))
131		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)))
132		oveq2 7459	. . . . . . . 8 ⊢ (𝑥 = (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)) → (1 / 𝑥) = (1 / (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))))
133	84, 130, 131, 132	fmptco 7162	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))) = (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (1 / (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))))
134	50, 41, 63, 81	recdivd 12150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {𝐶})) → (1 / (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶))) = ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶))))
135	134	mpteq2dva 5204	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (1 / (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))) = (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶)))))
136	133, 135	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))) = (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶)))))
137	136	oveq1d 7466	. . . . 5 ⊢ (𝜑 → (((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑦) − (𝐹‘𝐶)) / (𝑦 − 𝐶)))) lim_ℂ 𝐶) = ((𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶)))) lim_ℂ 𝐶))
138	124, 129, 137	3eltr3d 2878	. . . 4 ⊢ (𝜑 → (1 / ((𝑆 D 𝐹)‘𝐶)) ∈ ((𝑦 ∈ (𝑋 ∖ {𝐶}) ↦ ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶)))) lim_ℂ 𝐶))
139		oveq1 7458	. . . . 5 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑦 − 𝐶) = ((^◡𝐹‘𝑧) − 𝐶))
140		fveq2 6916	. . . . . 6 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
141	140	oveq1d 7466	. . . . 5 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝐹‘𝑦) − (𝐹‘𝐶)) = ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶)))
142	139, 141	oveq12d 7469	. . . 4 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝑦 − 𝐶) / ((𝐹‘𝑦) − (𝐹‘𝐶))) = (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶))))
143		eldifsni 4755	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) → 𝑧 ≠ (𝐹‘𝐶))
144	143	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → 𝑧 ≠ (𝐹‘𝐶))
145	144	necomd 3014	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → (𝐹‘𝐶) ≠ 𝑧)
146		f1ocnvfvb 7318	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶1-1onto𝑌 ∧ 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝐹‘𝐶) = 𝑧 ↔ (^◡𝐹‘𝑧) = 𝐶))
147	1, 4, 24, 146	syl2an3an 1450	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ((𝐹‘𝐶) = 𝑧 ↔ (^◡𝐹‘𝑧) = 𝐶))
148	147	necon3abid 2995	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ((𝐹‘𝐶) ≠ 𝑧 ↔ ¬ (^◡𝐹‘𝑧) = 𝐶))
149	145, 148	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ¬ (^◡𝐹‘𝑧) = 𝐶)
150	149	pm2.21d 122	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ((^◡𝐹‘𝑧) = 𝐶 → (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶))) = (1 / ((𝑆 D 𝐹)‘𝐶))))
151	150	impr 460	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ∧ (^◡𝐹‘𝑧) = 𝐶)) → (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶))) = (1 / ((𝑆 D 𝐹)‘𝐶)))
152	30, 64, 79, 138, 142, 151	limcco 26268	. . 3 ⊢ (𝜑 → (1 / ((𝑆 D 𝐹)‘𝐶)) ∈ ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶)))) lim_ℂ (𝐹‘𝐶)))
153	75	eqcomd 2769	. . . . . . . 8 ⊢ (𝜑 → 𝐶 = (^◡𝐹‘(𝐹‘𝐶)))
154	153	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → 𝐶 = (^◡𝐹‘(𝐹‘𝐶)))
155	154	oveq2d 7467	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ((^◡𝐹‘𝑧) − 𝐶) = ((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))))
156		f1ocnvfv2 7316	. . . . . . . 8 ⊢ ((𝐹:𝑋⟶1-1onto𝑌 ∧ 𝑧 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
157	1, 24, 156	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
158	157	oveq1d 7466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶)) = (𝑧 − (𝐹‘𝐶)))
159	155, 158	oveq12d 7469	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)})) → (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶))) = (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶))))
160	159	mpteq2dva 5204	. . . 4 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶)))) = (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶)))))
161	160	oveq1d 7466	. . 3 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − 𝐶) / ((𝐹‘(^◡𝐹‘𝑧)) − (𝐹‘𝐶)))) lim_ℂ (𝐹‘𝐶)) = ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶)))) lim_ℂ (𝐹‘𝐶)))
162	152, 161	eleqtrd 2866	. 2 ⊢ (𝜑 → (1 / ((𝑆 D 𝐹)‘𝐶)) ∈ ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶)))) lim_ℂ (𝐹‘𝐶)))
163		eqid 2763	. . 3 ⊢ (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶)))) = (𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶))))
164	23, 35	fssd 6757	. . 3 ⊢ (𝜑 → ^◡𝐹:𝑌⟶ℂ)
165	6, 7, 163, 11, 164, 43	eldv 26273	. 2 ⊢ (𝜑 → ((𝐹‘𝐶)(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘𝐶)) ↔ ((𝐹‘𝐶) ∈ ((int‘𝐾)‘𝑌) ∧ (1 / ((𝑆 D 𝐹)‘𝐶)) ∈ ((𝑧 ∈ (𝑌 ∖ {(𝐹‘𝐶)}) ↦ (((^◡𝐹‘𝑧) − (^◡𝐹‘(𝐹‘𝐶))) / (𝑧 − (𝐹‘𝐶)))) lim_ℂ (𝐹‘𝐶)))))
166	20, 162, 165	mpbir2and 726	1 ⊢ (𝜑 → (𝐹‘𝐶)(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘𝐶)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 {cpr 4590 class class class wbr 5108 ↦ cmpt 5192 ^◡ccnv 5657 dom cdm 5658 ran crn 5659 ↾ cres 5660 ∘ ccom 5662 Fun wfun 6560 Fn wfn 6561 ⟶wf 6562 ⟶1-1wf1 6563 ⟶1-1ontowf1o 6565 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 − cmin 11580 / cdiv 12013 ↾_t crest 17641 TopOpenctopn 17642 ℂ_fldccnfld 21729 Topctop 23266 TopOnctopon 23283 intcnt 23390 Cn ccn 23597 CnP ccnp 23598 ×_t ctx 23934 –cn→ccncf 25252 lim_ℂ climc 26237 D cdv 26238

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-icc 13523 df-fz 13680 df-fzo 13829 df-seq 14185 df-exp 14245 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-haus 23688 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-limc 26241 df-dv 26242

This theorem is used by: dvcnv 26352

W3C validator