![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > phnvi | Structured version Visualization version GIF version |
Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
phnvi.1 | ⊢ 𝑈 ∈ CPreHilOLD |
Ref | Expression |
---|---|
phnvi | ⊢ 𝑈 ∈ NrmCVec |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | phnvi.1 | . 2 ⊢ 𝑈 ∈ CPreHilOLD | |
2 | phnv 29994 | . 2 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑈 ∈ NrmCVec |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 NrmCVeccnv 29764 CPreHilOLDccphlo 29992 |
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-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3952 df-ss 3962 df-ph 29993 |
This theorem is referenced by: elimph 30000 ip0i 30005 ip1ilem 30006 ip2i 30008 ipdirilem 30009 ipasslem1 30011 ipasslem2 30012 ipasslem4 30014 ipasslem5 30015 ipasslem7 30016 ipasslem8 30017 ipasslem9 30018 ipasslem10 30019 ipasslem11 30020 ip2dii 30024 pythi 30030 siilem1 30031 siilem2 30032 siii 30033 ipblnfi 30035 ip2eqi 30036 ajfuni 30039 |
Copyright terms: Public domain | W3C validator |