![]() |
Mathbox for Steve Rodriguez |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sblpnf | Structured version Visualization version GIF version |
Description: The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 22324. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
Ref | Expression |
---|---|
sblpnf.s | ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
sblpnf.d | ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) |
Ref | Expression |
---|---|
sblpnf | ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sblpnf.s | . . 3 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | |
2 | elpri 4305 | . . 3 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ)) | |
3 | sblpnf.d | . . . . 5 ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) | |
4 | eqid 2724 | . . . . . . 7 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ)) | |
5 | 4 | remet 22715 | . . . . . 6 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ) |
6 | xpeq12 5243 | . . . . . . . . 9 ⊢ ((𝑆 = ℝ ∧ 𝑆 = ℝ) → (𝑆 × 𝑆) = (ℝ × ℝ)) | |
7 | 6 | anidms 680 | . . . . . . . 8 ⊢ (𝑆 = ℝ → (𝑆 × 𝑆) = (ℝ × ℝ)) |
8 | 7 | reseq2d 5503 | . . . . . . 7 ⊢ (𝑆 = ℝ → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (ℝ × ℝ))) |
9 | fveq2 6304 | . . . . . . 7 ⊢ (𝑆 = ℝ → (Met‘𝑆) = (Met‘ℝ)) | |
10 | 8, 9 | eleq12d 2797 | . . . . . 6 ⊢ (𝑆 = ℝ → (((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆) ↔ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ))) |
11 | 5, 10 | mpbiri 248 | . . . . 5 ⊢ (𝑆 = ℝ → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆)) |
12 | 3, 11 | syl5eqel 2807 | . . . 4 ⊢ (𝑆 = ℝ → 𝐷 ∈ (Met‘𝑆)) |
13 | relco 5746 | . . . . . . . . 9 ⊢ Rel (abs ∘ − ) | |
14 | resdm 5551 | . . . . . . . . 9 ⊢ (Rel (abs ∘ − ) → ((abs ∘ − ) ↾ dom (abs ∘ − )) = (abs ∘ − )) | |
15 | 13, 14 | ax-mp 5 | . . . . . . . 8 ⊢ ((abs ∘ − ) ↾ dom (abs ∘ − )) = (abs ∘ − ) |
16 | absf 14197 | . . . . . . . . . . . 12 ⊢ abs:ℂ⟶ℝ | |
17 | ax-resscn 10106 | . . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ | |
18 | fss 6169 | . . . . . . . . . . . 12 ⊢ ((abs:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → abs:ℂ⟶ℂ) | |
19 | 16, 17, 18 | mp2an 710 | . . . . . . . . . . 11 ⊢ abs:ℂ⟶ℂ |
20 | subf 10396 | . . . . . . . . . . 11 ⊢ − :(ℂ × ℂ)⟶ℂ | |
21 | fco 6171 | . . . . . . . . . . 11 ⊢ ((abs:ℂ⟶ℂ ∧ − :(ℂ × ℂ)⟶ℂ) → (abs ∘ − ):(ℂ × ℂ)⟶ℂ) | |
22 | 19, 20, 21 | mp2an 710 | . . . . . . . . . 10 ⊢ (abs ∘ − ):(ℂ × ℂ)⟶ℂ |
23 | 22 | fdmi 6165 | . . . . . . . . 9 ⊢ dom (abs ∘ − ) = (ℂ × ℂ) |
24 | 23 | reseq2i 5500 | . . . . . . . 8 ⊢ ((abs ∘ − ) ↾ dom (abs ∘ − )) = ((abs ∘ − ) ↾ (ℂ × ℂ)) |
25 | 15, 24 | eqtr3i 2748 | . . . . . . 7 ⊢ (abs ∘ − ) = ((abs ∘ − ) ↾ (ℂ × ℂ)) |
26 | cnmet 22697 | . . . . . . 7 ⊢ (abs ∘ − ) ∈ (Met‘ℂ) | |
27 | 25, 26 | eqeltrri 2800 | . . . . . 6 ⊢ ((abs ∘ − ) ↾ (ℂ × ℂ)) ∈ (Met‘ℂ) |
28 | xpeq12 5243 | . . . . . . . . 9 ⊢ ((𝑆 = ℂ ∧ 𝑆 = ℂ) → (𝑆 × 𝑆) = (ℂ × ℂ)) | |
29 | 28 | anidms 680 | . . . . . . . 8 ⊢ (𝑆 = ℂ → (𝑆 × 𝑆) = (ℂ × ℂ)) |
30 | 29 | reseq2d 5503 | . . . . . . 7 ⊢ (𝑆 = ℂ → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (ℂ × ℂ))) |
31 | fveq2 6304 | . . . . . . 7 ⊢ (𝑆 = ℂ → (Met‘𝑆) = (Met‘ℂ)) | |
32 | 30, 31 | eleq12d 2797 | . . . . . 6 ⊢ (𝑆 = ℂ → (((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆) ↔ ((abs ∘ − ) ↾ (ℂ × ℂ)) ∈ (Met‘ℂ))) |
33 | 27, 32 | mpbiri 248 | . . . . 5 ⊢ (𝑆 = ℂ → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆)) |
34 | 3, 33 | syl5eqel 2807 | . . . 4 ⊢ (𝑆 = ℂ → 𝐷 ∈ (Met‘𝑆)) |
35 | 12, 34 | jaoi 393 | . . 3 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝐷 ∈ (Met‘𝑆)) |
36 | 1, 2, 35 | 3syl 18 | . 2 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑆)) |
37 | blpnf 22324 | . 2 ⊢ ((𝐷 ∈ (Met‘𝑆) ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) | |
38 | 36, 37 | sylan 489 | 1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 = wceq 1596 ∈ wcel 2103 ⊆ wss 3680 {cpr 4287 × cxp 5216 dom cdm 5218 ↾ cres 5220 ∘ ccom 5222 Rel wrel 5223 ⟶wf 5997 ‘cfv 6001 (class class class)co 6765 ℂcc 10047 ℝcr 10048 +∞cpnf 10184 − cmin 10379 abscabs 14094 Metcme 19855 ballcbl 19856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126 ax-pre-sup 10127 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-om 7183 df-1st 7285 df-2nd 7286 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-er 7862 df-map 7976 df-en 8073 df-dom 8074 df-sdom 8075 df-sup 8464 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-div 10798 df-nn 11134 df-2 11192 df-3 11193 df-n0 11406 df-z 11491 df-uz 11801 df-rp 11947 df-xneg 12060 df-xadd 12061 df-xmul 12062 df-seq 12917 df-exp 12976 df-cj 13959 df-re 13960 df-im 13961 df-sqrt 14095 df-abs 14096 df-psmet 19861 df-xmet 19862 df-met 19863 df-bl 19864 |
This theorem is referenced by: dvconstbi 38952 |
Copyright terms: Public domain | W3C validator |