![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iscbn | Structured version Visualization version GIF version |
Description: A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 23628 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
iscbn.x | ⊢ 𝑋 = (BaseSet‘𝑈) |
iscbn.8 | ⊢ 𝐷 = (IndMet‘𝑈) |
Ref | Expression |
---|---|
iscbn | ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6545 | . . . 4 ⊢ (𝑢 = 𝑈 → (IndMet‘𝑢) = (IndMet‘𝑈)) | |
2 | iscbn.8 | . . . 4 ⊢ 𝐷 = (IndMet‘𝑈) | |
3 | 1, 2 | syl6eqr 2851 | . . 3 ⊢ (𝑢 = 𝑈 → (IndMet‘𝑢) = 𝐷) |
4 | fveq2 6545 | . . . . 5 ⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = (BaseSet‘𝑈)) | |
5 | iscbn.x | . . . . 5 ⊢ 𝑋 = (BaseSet‘𝑈) | |
6 | 4, 5 | syl6eqr 2851 | . . . 4 ⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = 𝑋) |
7 | 6 | fveq2d 6549 | . . 3 ⊢ (𝑢 = 𝑈 → (CMet‘(BaseSet‘𝑢)) = (CMet‘𝑋)) |
8 | 3, 7 | eleq12d 2879 | . 2 ⊢ (𝑢 = 𝑈 → ((IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢)) ↔ 𝐷 ∈ (CMet‘𝑋))) |
9 | df-cbn 28327 | . 2 ⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))} | |
10 | 8, 9 | elrab2 3624 | 1 ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ‘cfv 6232 CMetccmet 23544 NrmCVeccnv 28048 BaseSetcba 28050 IndMetcims 28055 CBanccbn 28326 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-rex 3113 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-iota 6196 df-fv 6240 df-cbn 28327 |
This theorem is referenced by: cbncms 28329 bnnv 28330 bnsscmcl 28332 cnbn 28333 hhhl 28668 hhssbnOLD 28743 |
Copyright terms: Public domain | W3C validator |