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 26205

Description: A weak version of dvcnvre 26247, 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 26134	. . . . 5 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
3	1, 2	syl 18	. . . 4 ⊢ (𝜑 → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
4		recnprss 26132	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
5	1, 4	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvcnv.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)
7		f1ocnv 6831	. . . . . . . . 9 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
8		f1of 6818	. . . . . . . . 9 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
9	6, 7, 8	3syl 19	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
10		dvcnv.d	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
11		dvbsss 26130	. . . . . . . . . 10 ⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
12	10, 11	eqsstrrdi 3976	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
13	12, 5	sstrd 3941	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
14	9, 13	fssd 6721	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑌⟶ℂ)
15		dvcnv.k	. . . . . . . . 9 ⊢ 𝐾 = (𝐽 ↾_t 𝑆)
16		dvcnv.j	. . . . . . . . . . 11 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
17	16	cnfldtopon 25009	. . . . . . . . . 10 ⊢ 𝐽 ∈ (TopOn‘ℂ)
18		resttopon 23387	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
19	17, 5, 18	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
20	15, 19	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑆))
21		dvcnv.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
22		toponss 23153	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘𝑆) ∧ 𝑌 ∈ 𝐾) → 𝑌 ⊆ 𝑆)
23	20, 21, 22	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
24	5, 14, 23	dvbss 26129	. . . . . 6 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) ⊆ 𝑌)
25		f1ocnvfv2 7279	. . . . . . . . 9 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
26	6, 25	sylan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
27	1	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ {ℝ, ℂ})
28	21	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑌 ∈ 𝐾)
29	6	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
30		dvcnv.i	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
31	30	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ (𝑌–cn→𝑋))
32	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → dom (𝑆 D 𝐹) = 𝑋)
33		dvcnv.z	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))
34	33	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ¬ 0 ∈ ran (𝑆 D 𝐹))
35	9	ffvelcdmda 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
36	16, 15, 27, 28, 29, 31, 32, 34, 35	dvcnvlem 26204	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥))(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
37	26, 36	eqbrtrrd 5129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
38		reldv 26098	. . . . . . . 8 ⊢ Rel (𝑆 D ^◡𝐹)
39	38	releldmi 5932	. . . . . . 7 ⊢ (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
40	37, 39	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
41	24, 40	eqelssd 3952	. . . . 5 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) = 𝑌)
42	41	feq2d 6687	. . . 4 ⊢ (𝜑 → ((𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ ↔ (𝑆 D ^◡𝐹):𝑌⟶ℂ))
43	3, 42	mpbid 235	. . 3 ⊢ (𝜑 → (𝑆 D ^◡𝐹):𝑌⟶ℂ)
44	43	feqmptd 6947	. 2 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)))
45	3	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
46	45	ffund 6708	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → Fun (𝑆 D ^◡𝐹))
47		funbrfv 6927	. . . 4 ⊢ (Fun (𝑆 D ^◡𝐹) → (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
48	46, 37, 47	sylc 66	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
49	48	mpteq2dva 5198	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
50	44, 49	eqtrd 2795	1 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ⊆ wss 3899 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 ^◡ccnv 5654 dom cdm 5655 ran crn 5656 Fun wfun 6527 ⟶wf 6529 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7414 ℂcc 11123 ℝcr 11124 0cc0 11125 1c1 11126 / cdiv 11896 ↾_t crest 17506 TopOpenctopn 17507 ℂ_fldccnfld 21586 TopOnctopon 23136 –cn→ccncf 25105 D cdv 26091

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-2o 8457 df-er 8697 df-map 8829 df-pm 8830 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9333 df-fi 9382 df-sup 9413 df-inf 9414 df-oi 9483 df-card 9945 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-q 12999 df-rp 13044 df-xneg 13164 df-xadd 13165 df-xmul 13166 df-icc 13406 df-fz 13563 df-fzo 13711 df-seq 14067 df-exp 14127 df-hash 14396 df-cj 15187 df-re 15188 df-im 15189 df-sqrt 15323 df-abs 15324 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-starv 17358 df-sca 17359 df-vsca 17360 df-ip 17361 df-tset 17362 df-ple 17363 df-ds 17365 df-unif 17366 df-hom 17367 df-cco 17368 df-rest 17508 df-topn 17509 df-0g 17527 df-gsum 17528 df-topgen 17529 df-pt 17530 df-prds 17533 df-xrs 17589 df-qtop 17594 df-imas 17595 df-xps 17597 df-mre 17671 df-mrc 17672 df-acs 17674 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-limc 26094 df-dv 26095

This theorem is used by: dvcnvre 26247 dvlog 26889

W3C validator