![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cncfcdm | Structured version Visualization version GIF version |
Description: Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
Ref | Expression |
---|---|
cncfcdm | ⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ 𝐹:𝐴⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncfi 24294 | . . . . 5 ⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)) | |
2 | 1 | 3expb 1120 | . . . 4 ⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)) |
3 | 2 | ralrimivva 3193 | . . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)) |
4 | 3 | adantl 482 | . 2 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)) |
5 | cncfrss 24291 | . . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
6 | simpl 483 | . . 3 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐶 ⊆ ℂ) | |
7 | elcncf2 24290 | . . 3 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ (𝐹:𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) | |
8 | 5, 6, 7 | syl2an2 684 | . 2 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ (𝐹:𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) |
9 | 4, 8 | mpbiran2d 706 | 1 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ 𝐹:𝐴⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 ⊆ wss 3913 class class class wbr 5110 ⟶wf 6497 ‘cfv 6501 (class class class)co 7362 ℂcc 11058 < clt 11198 − cmin 11394 ℝ+crp 12924 abscabs 15131 –cn→ccncf 24276 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-cnex 11116 ax-resscn 11117 ax-1cn 11118 ax-icn 11119 ax-addcl 11120 ax-addrcl 11121 ax-mulcl 11122 ax-mulrcl 11123 ax-mulcom 11124 ax-addass 11125 ax-mulass 11126 ax-distr 11127 ax-i2m1 11128 ax-1ne0 11129 ax-1rid 11130 ax-rnegex 11131 ax-rrecex 11132 ax-cnre 11133 ax-pre-lttri 11134 ax-pre-lttrn 11135 ax-pre-ltadd 11136 ax-pre-mulgt0 11137 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-er 8655 df-map 8774 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-sub 11396 df-neg 11397 df-div 11822 df-2 12225 df-cj 14996 df-re 14997 df-im 14998 df-abs 15133 df-cncf 24278 |
This theorem is referenced by: cncfss 24299 cncfmpt2ss 24316 rolle 25391 dvlipcn 25395 c1lip2 25399 dvivthlem1 25409 dvivth 25411 lhop1lem 25414 dvcnvrelem2 25419 dvfsumlem2 25428 itgsubstlem 25449 efcvx 25845 dvrelog 26029 relogcn 26030 logcn 26039 dvlog 26043 logccv 26055 resqrtcn 26139 loglesqrt 26148 lgamgulmlem2 26416 rpsqrtcn 33295 fdvneggt 33302 fdvnegge 33304 logdivsqrle 33352 knoppcn2 35075 areacirclem4 36242 cncfres 36297 intlewftc 40591 aks4d1p1p5 40605 cncfmptssg 44232 resincncf 44236 cncfcompt 44244 cncfiooiccre 44256 dvdivcncf 44288 dvbdfbdioolem1 44289 ioodvbdlimc1lem2 44293 ioodvbdlimc2lem 44295 itgsbtaddcnst 44343 fourierdlem58 44525 fourierdlem59 44526 fourierdlem62 44529 fourierdlem68 44535 fourierdlem76 44543 fourierdlem78 44545 fourierdlem83 44550 fourierdlem101 44568 fourierdlem112 44579 fouriercn 44593 |
Copyright terms: Public domain | W3C validator |