dvcnvre - Metamath Proof Explorer

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

Theorem dvcnvre 25536

Description: The derivative rule for inverse functions. If 𝐹 is a continuous and differentiable bijective function from 𝑋 to 𝑌 which never has derivative 0, then ^◡𝐹 is also differentiable, and its derivative is the reciprocal of the derivative of 𝐹. (Contributed by Mario Carneiro, 24-Feb-2015.)

**Hypotheses**
Ref	Expression
dvcnvre.f	⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))
dvcnvre.d	⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)
dvcnvre.z	⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
dvcnvre.1	⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)

**Assertion**
Ref	Expression
dvcnvre	⊢ (𝜑 → (ℝ D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(^◡𝐹‘𝑥)))))

Distinct variable groups: 𝑥,𝐹 𝜑,𝑥 𝑥,𝑋 𝑥,𝑌

Proof of Theorem dvcnvre Dummy variables 𝑦 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2733	. 2 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
2	1	tgioo2 24319	. 2 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
3		reelprrecn 11202	. . 3 ⊢ ℝ ∈ {ℝ, ℂ}
4	3	a1i 11	. 2 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
5		retop 24278	. . . . 5 ⊢ (topGen‘ran (,)) ∈ Top
6		dvcnvre.1	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)
7		f1ofo 6841	. . . . . . 7 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌)
8		forn 6809	. . . . . . 7 ⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌)
9	6, 7, 8	3syl 18	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝑌)
10		dvcnvre.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))
11		cncff 24409	. . . . . . 7 ⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ)
12		frn 6725	. . . . . . 7 ⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ)
13	10, 11, 12	3syl 18	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
14	9, 13	eqsstrrd 4022	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ ℝ)
15		uniretop 24279	. . . . . 6 ⊢ ℝ = ∪ (topGen‘ran (,))
16	15	ntrss2 22561	. . . . 5 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌)
17	5, 14, 16	sylancr 588	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌)
18		f1ocnvfv2 7275	. . . . . 6 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
19	6, 18	sylan 581	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
20		eqid 2733	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
21	20	rexmet 24307	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
22		dvcnvre.d	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)
23		dvbsss 25419	. . . . . . . . . . . . 13 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
24	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
25	22, 24	eqsstrrd 4022	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
26	15	ntrss2 22561	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋)
27	5, 25, 26	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋)
28		ax-resscn 11167	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
31		fss 6735	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝑋⟶ℂ)
32	30, 28, 31	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
33	29, 32, 25, 2, 1	dvbssntr 25417	. . . . . . . . . . 11 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
34	22, 33	eqsstrrd 4022	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
35	27, 34	eqssd 4000	. . . . . . . . 9 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋)
36	15	isopn3 22570	. . . . . . . . . 10 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) → (𝑋 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋))
37	5, 25, 36	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋))
38	35, 37	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ (topGen‘ran (,)))
39		f1ocnv 6846	. . . . . . . . . 10 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6834	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
41	6, 39, 40	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
42	41	ffvelcdmda 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
43		eqid 2733	. . . . . . . . . 10 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
44	20, 43	tgioo 24312	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
45	44	mopni2 24002	. . . . . . . 8 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝑋 ∈ (topGen‘ran (,)) ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
46	21, 38, 42, 45	mp3an2ani 1469	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
47	10	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹 ∈ (𝑋–cn→ℝ))
48	22	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → dom (ℝ D 𝐹) = 𝑋)
49		dvcnvre.z	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
50	49	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐹))
51	6	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹:𝑋–1-1-onto→𝑌)
52	42	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (^◡𝐹‘𝑥) ∈ 𝑋)
53		rphalfcl 13001	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) ∈ ℝ⁺)
54	53	ad2antrl 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈ ℝ⁺)
55	25	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑋 ⊆ ℝ)
56	55, 52	sseldd 3984	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (^◡𝐹‘𝑥) ∈ ℝ)
57	54	rpred 13016	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈ ℝ)
58	56, 57	resubcld 11642	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ)
59	56, 57	readdcld 11243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ)
60		elicc2 13389	. . . . . . . . . . . . . . . 16 ⊢ ((((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ ∧ ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))))
61	58, 59, 60	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))))
62	61	biimpa 478	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2))))
63	62	simp1d 1143	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ ℝ)
64	56	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (^◡𝐹‘𝑥) ∈ ℝ)
65		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ⁺)
66	65	rpred 13016	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ)
67	64, 66	resubcld 11642	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ)
68	58	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ)
69	65, 53	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ⁺)
70	69	rpred 13016	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ)
71		rphalflt 13003	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
72	65, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) < 𝑟)
73	70, 66, 64, 72	ltsub2dd 11827	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) < ((^◡𝐹‘𝑥) − (𝑟 / 2)))
74	62	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦)
75	67, 68, 63, 73, 74	ltletrd 11374	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) < 𝑦)
76	59	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ)
77	64, 66	readdcld 11243	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ)
78	62	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))
79	70, 66, 64, 72	ltadd2dd 11373	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) < ((^◡𝐹‘𝑥) + 𝑟))
80	63, 76, 77, 78, 79	lelttrd 11372	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))
81	67	rexrd 11264	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ^*)
82	77	rexrd 11264	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ^*)
83		elioo2 13365	. . . . . . . . . . . . . 14 ⊢ ((((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ^* ∧ ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ^*) → (𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))))
84	81, 82, 83	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))))
85	63, 75, 80, 84	mpbir3and 1343	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
86	85	ex 414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) → 𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟))))
87	86	ssrdv 3989	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
88		rpre 12982	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
89	88	ad2antrl 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑟 ∈ ℝ)
90	20	bl2ioo 24308	. . . . . . . . . . 11 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
91	56, 89, 90	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
92	87, 91	sseqtrrd 4024	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟))
93		simprr 772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
94	92, 93	sstrd 3993	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ 𝑋)
95		eqid 2733	. . . . . . . 8 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
96		eqid 2733	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑋) = ((TopOpen‘ℂ_fld) ↾_t 𝑋)
97		eqid 2733	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑌) = ((TopOpen‘ℂ_fld) ↾_t 𝑌)
98	47, 48, 50, 51, 52, 54, 94, 95, 1, 96, 97	dvcnvrelem2 25535	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌) ∧ ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥)))))
99	46, 98	rexlimddv 3162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌) ∧ ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥)))))
100	99	simpld 496	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌))
101	19, 100	eqeltrrd 2835	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ ((int‘(topGen‘ran (,)))‘𝑌))
102	17, 101	eqelssd 4004	. . 3 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌)
103	15	isopn3 22570	. . . 4 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌))
104	5, 14, 103	sylancr 588	. . 3 ⊢ (𝜑 → (𝑌 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌))
105	102, 104	mpbird 257	. 2 ⊢ (𝜑 → 𝑌 ∈ (topGen‘ran (,)))
106	99	simprd 497	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥))))
107	19	fveq2d 6896	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥))) = ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
108	106, 107	eleqtrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
109	108	ralrimiva 3147	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
110	1	cnfldtopon 24299	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
111	14, 28	sstrdi 3995	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
112		resttopon 22665	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌))
113	110, 111, 112	sylancr 588	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌))
114	25, 28	sstrdi 3995	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
115		resttopon 22665	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑋 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋))
116	110, 114, 115	sylancr 588	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋))
117		cncnp 22784	. . . . 5 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌) ∧ ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋)) → (^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)) ↔ (^◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))))
118	113, 116, 117	syl2anc 585	. . . 4 ⊢ (𝜑 → (^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)) ↔ (^◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))))
119	41, 109, 118	mpbir2and 712	. . 3 ⊢ (𝜑 → ^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
120	1, 97, 96	cncfcn 24426	. . . 4 ⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ) → (𝑌–cn→𝑋) = (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
121	111, 114, 120	syl2anc 585	. . 3 ⊢ (𝜑 → (𝑌–cn→𝑋) = (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
122	119, 121	eleqtrrd 2837	. 2 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
123	1, 2, 4, 105, 6, 122, 22, 49	dvcnv 25494	1 ⊢ (𝜑 → (ℝ D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(^◡𝐹‘𝑥)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 ⊆ wss 3949 {cpr 4631 class class class wbr 5149 ↦ cmpt 5232 × cxp 5675 ^◡ccnv 5676 dom cdm 5677 ran crn 5678 ↾ cres 5679 ∘ ccom 5681 ⟶wf 6540 –onto→wfo 6542 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 ℂcc 11108 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 ℝ^*cxr 11247 < clt 11248 ≤ cle 11249 − cmin 11444 / cdiv 11871 2c2 12267 ℝ⁺crp 12974 (,)cioo 13324 [,]cicc 13327 abscabs 15181 ↾_t crest 17366 TopOpenctopn 17367 topGenctg 17383 ∞Metcxmet 20929 ballcbl 20931 MetOpencmopn 20934 ℂ_fldccnfld 20944 Topctop 22395 TopOnctopon 22412 intcnt 22521 Cn ccn 22728 CnP ccnp 22729 –cn→ccncf 24392 D cdv 25380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188 ax-addf 11189 ax-mulf 11190

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7670 df-om 7856 df-1st 7975 df-2nd 7976 df-supp 8147 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-2o 8467 df-er 8703 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9362 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9505 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-q 12933 df-rp 12975 df-xneg 13092 df-xadd 13093 df-xmul 13094 df-ioo 13328 df-ico 13330 df-icc 13331 df-fz 13485 df-fzo 13628 df-seq 13967 df-exp 14028 df-hash 14291 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-struct 17080 df-sets 17097 df-slot 17115 df-ndx 17127 df-base 17145 df-ress 17174 df-plusg 17210 df-mulr 17211 df-starv 17212 df-sca 17213 df-vsca 17214 df-ip 17215 df-tset 17216 df-ple 17217 df-ds 17219 df-unif 17220 df-hom 17221 df-cco 17222 df-rest 17368 df-topn 17369 df-0g 17387 df-gsum 17388 df-topgen 17389 df-pt 17390 df-prds 17393 df-xrs 17448 df-qtop 17453 df-imas 17454 df-xps 17456 df-mre 17530 df-mrc 17531 df-acs 17533 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-submnd 18672 df-mulg 18951 df-cntz 19181 df-cmn 19650 df-psmet 20936 df-xmet 20937 df-met 20938 df-bl 20939 df-mopn 20940 df-fbas 20941 df-fg 20942 df-cnfld 20945 df-top 22396 df-topon 22413 df-topsp 22435 df-bases 22449 df-cld 22523 df-ntr 22524 df-cls 22525 df-nei 22602 df-lp 22640 df-perf 22641 df-cn 22731 df-cnp 22732 df-haus 22819 df-cmp 22891 df-tx 23066 df-hmeo 23259 df-fil 23350 df-fm 23442 df-flim 23443 df-flf 23444 df-xms 23826 df-ms 23827 df-tms 23828 df-cncf 24394 df-limc 25383 df-dv 25384

This theorem is referenced by: dvrelog 26145

W3C validator