dvcnv - Metamath Proof Explorer

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

Theorem dvcnv 23959

Description: A weak version of dvcnvre 24001, valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (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-1-onto→𝑌)
dvcnv.i	⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
dvcnv.d	⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
dvcnv.z	⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))

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

Distinct variable groups: 𝑥,𝐹 𝑥,𝐽 𝜑,𝑥 𝑥,𝑆 𝑥,𝑌 Allowed substitution hints: 𝐾(𝑥) 𝑋(𝑥)

**Proof of Theorem dvcnv**
Step	Hyp	Ref	Expression
1		dvcnv.s	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
2		dvfg 23889	. . . . 5 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
4		recnprss 23887	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvcnv.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)
7		f1ocnv 6290	. . . . . . . . 9 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
8		f1of 6278	. . . . . . . . 9 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
9	6, 7, 8	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
10		dvcnv.d	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
11		dvbsss 23885	. . . . . . . . . 10 ⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
12	10, 11	syl6eqssr 3803	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
13	12, 5	sstrd 3760	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
14	9, 13	fssd 6197	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑌⟶ℂ)
15		dvcnv.k	. . . . . . . . 9 ⊢ 𝐾 = (𝐽 ↾_t 𝑆)
16		dvcnv.j	. . . . . . . . . . 11 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
17	16	cnfldtopon 22805	. . . . . . . . . 10 ⊢ 𝐽 ∈ (TopOn‘ℂ)
18		resttopon 21185	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
19	17, 5, 18	sylancr 567	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
20	15, 19	syl5eqel 2853	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑆))
21		dvcnv.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
22		toponss 20951	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘𝑆) ∧ 𝑌 ∈ 𝐾) → 𝑌 ⊆ 𝑆)
23	20, 21, 22	syl2anc 565	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
24	5, 14, 23	dvbss 23884	. . . . . 6 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) ⊆ 𝑌)
25		f1ocnvfv2 6675	. . . . . . . . . . 11 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
26	6, 25	sylan 561	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
27	1	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ {ℝ, ℂ})
28	21	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑌 ∈ 𝐾)
29	6	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
30		dvcnv.i	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
31	30	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ (𝑌–cn→𝑋))
32	10	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → dom (𝑆 D 𝐹) = 𝑋)
33		dvcnv.z	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))
34	33	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ¬ 0 ∈ ran (𝑆 D 𝐹))
35	9	ffvelrnda 6502	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
36	16, 15, 27, 28, 29, 31, 32, 34, 35	dvcnvlem 23958	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥))(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
37	26, 36	eqbrtrrd 4808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
38		reldv 23853	. . . . . . . . . 10 ⊢ Rel (𝑆 D ^◡𝐹)
39	38	releldmi 5500	. . . . . . . . 9 ⊢ (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
40	37, 39	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
41	40	ex 397	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝑌 → 𝑥 ∈ dom (𝑆 D ^◡𝐹)))
42	41	ssrdv 3756	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ dom (𝑆 D ^◡𝐹))
43	24, 42	eqssd 3767	. . . . 5 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) = 𝑌)
44	43	feq2d 6171	. . . 4 ⊢ (𝜑 → ((𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ ↔ (𝑆 D ^◡𝐹):𝑌⟶ℂ))
45	3, 44	mpbid 222	. . 3 ⊢ (𝜑 → (𝑆 D ^◡𝐹):𝑌⟶ℂ)
46	45	feqmptd 6391	. 2 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)))
47	3	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
48		ffun 6188	. . . . 5 ⊢ ((𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ → Fun (𝑆 D ^◡𝐹))
49	47, 48	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → Fun (𝑆 D ^◡𝐹))
50		funbrfv 6375	. . . 4 ⊢ (Fun (𝑆 D ^◡𝐹) → (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
51	49, 37, 50	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
52	51	mpteq2dva 4876	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
53	46, 52	eqtrd 2804	1 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 382 = wceq 1630 ∈ wcel 2144 ⊆ wss 3721 {cpr 4316 class class class wbr 4784 ↦ cmpt 4861 ^◡ccnv 5248 dom cdm 5249 ran crn 5250 Fun wfun 6025 ⟶wf 6027 –1-1-onto→wf1o 6030 ‘cfv 6031 (class class class)co 6792 ℂcc 10135 ℝcr 10136 0cc0 10137 1c1 10138 / cdiv 10885 ↾_t crest 16288 TopOpenctopn 16289 ℂ_fldccnfld 19960 TopOnctopon 20934 –cn→ccncf 22898 D cdv 23846

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-8 2146 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-rep 4902 ax-sep 4912 ax-nul 4920 ax-pow 4971 ax-pr 5034 ax-un 7095 ax-inf2 8701 ax-cnex 10193 ax-resscn 10194 ax-1cn 10195 ax-icn 10196 ax-addcl 10197 ax-addrcl 10198 ax-mulcl 10199 ax-mulrcl 10200 ax-mulcom 10201 ax-addass 10202 ax-mulass 10203 ax-distr 10204 ax-i2m1 10205 ax-1ne0 10206 ax-1rid 10207 ax-rnegex 10208 ax-rrecex 10209 ax-cnre 10210 ax-pre-lttri 10211 ax-pre-lttrn 10212 ax-pre-ltadd 10213 ax-pre-mulgt0 10214 ax-pre-sup 10215 ax-mulf 10217

This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3or 1071 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ne 2943 df-nel 3046 df-ral 3065 df-rex 3066 df-reu 3067 df-rmo 3068 df-rab 3069 df-v 3351 df-sbc 3586 df-csb 3681 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-pss 3737 df-nul 4062 df-if 4224 df-pw 4297 df-sn 4315 df-pr 4317 df-tp 4319 df-op 4321 df-uni 4573 df-int 4610 df-iun 4654 df-iin 4655 df-br 4785 df-opab 4845 df-mpt 4862 df-tr 4885 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-isom 6040 df-riota 6753 df-ov 6795 df-oprab 6796 df-mpt2 6797 df-of 7043 df-om 7212 df-1st 7314 df-2nd 7315 df-supp 7446 df-wrecs 7558 df-recs 7620 df-rdg 7658 df-1o 7712 df-2o 7713 df-oadd 7716 df-er 7895 df-map 8010 df-pm 8011 df-ixp 8062 df-en 8109 df-dom 8110 df-sdom 8111 df-fin 8112 df-fsupp 8431 df-fi 8472 df-sup 8503 df-inf 8504 df-oi 8570 df-card 8964 df-cda 9191 df-pnf 10277 df-mnf 10278 df-xr 10279 df-ltxr 10280 df-le 10281 df-sub 10469 df-neg 10470 df-div 10886 df-nn 11222 df-2 11280 df-3 11281 df-4 11282 df-5 11283 df-6 11284 df-7 11285 df-8 11286 df-9 11287 df-n0 11494 df-z 11579 df-dec 11695 df-uz 11888 df-q 11991 df-rp 12035 df-xneg 12150 df-xadd 12151 df-xmul 12152 df-icc 12386 df-fz 12533 df-fzo 12673 df-seq 13008 df-exp 13067 df-hash 13321 df-cj 14046 df-re 14047 df-im 14048 df-sqrt 14182 df-abs 14183 df-struct 16065 df-ndx 16066 df-slot 16067 df-base 16069 df-sets 16070 df-ress 16071 df-plusg 16161 df-mulr 16162 df-starv 16163 df-sca 16164 df-vsca 16165 df-ip 16166 df-tset 16167 df-ple 16168 df-ds 16171 df-unif 16172 df-hom 16173 df-cco 16174 df-rest 16290 df-topn 16291 df-0g 16309 df-gsum 16310 df-topgen 16311 df-pt 16312 df-prds 16315 df-xrs 16369 df-qtop 16374 df-imas 16375 df-xps 16377 df-mre 16453 df-mrc 16454 df-acs 16456 df-mgm 17449 df-sgrp 17491 df-mnd 17502 df-submnd 17543 df-mulg 17748 df-cntz 17956 df-cmn 18401 df-psmet 19952 df-xmet 19953 df-met 19954 df-bl 19955 df-mopn 19956 df-fbas 19957 df-fg 19958 df-cnfld 19961 df-top 20918 df-topon 20935 df-topsp 20957 df-bases 20970 df-cld 21043 df-ntr 21044 df-cls 21045 df-nei 21122 df-lp 21160 df-perf 21161 df-cn 21251 df-cnp 21252 df-haus 21339 df-tx 21585 df-hmeo 21778 df-fil 21869 df-fm 21961 df-flim 21962 df-flf 21963 df-xms 22344 df-ms 22345 df-tms 22346 df-cncf 22900 df-limc 23849 df-dv 23850

This theorem is referenced by: dvcnvre 24001 dvlog 24617

W3C validator