![]() |
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 28594 | . 2 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑈 ∈ NrmCVec |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 NrmCVeccnv 28364 CPreHilOLDccphlo 28592 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-in 3946 df-ss 3955 df-ph 28593 |
This theorem is referenced by: elimph 28600 ip0i 28605 ip1ilem 28606 ip2i 28608 ipdirilem 28609 ipasslem1 28611 ipasslem2 28612 ipasslem4 28614 ipasslem5 28615 ipasslem7 28616 ipasslem8 28617 ipasslem9 28618 ipasslem10 28619 ipasslem11 28620 ip2dii 28624 pythi 28630 siilem1 28631 siilem2 28632 siii 28633 ipblnfi 28635 ip2eqi 28636 ajfuni 28639 |
Copyright terms: Public domain | W3C validator |