![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > phnv | Structured version Visualization version GIF version |
Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
phnv | โข (๐ โ CPreHilOLD โ ๐ โ NrmCVec) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ph 30066 | . . 3 โข CPreHilOLD = (NrmCVec โฉ {โจโจ๐, ๐ โฉ, ๐โฉ โฃ โ๐ฅ โ ran ๐โ๐ฆ โ ran ๐(((๐โ(๐ฅ๐๐ฆ))โ2) + ((๐โ(๐ฅ๐(-1๐ ๐ฆ)))โ2)) = (2 ยท (((๐โ๐ฅ)โ2) + ((๐โ๐ฆ)โ2)))}) | |
2 | inss1 4229 | . . 3 โข (NrmCVec โฉ {โจโจ๐, ๐ โฉ, ๐โฉ โฃ โ๐ฅ โ ran ๐โ๐ฆ โ ran ๐(((๐โ(๐ฅ๐๐ฆ))โ2) + ((๐โ(๐ฅ๐(-1๐ ๐ฆ)))โ2)) = (2 ยท (((๐โ๐ฅ)โ2) + ((๐โ๐ฆ)โ2)))}) โ NrmCVec | |
3 | 1, 2 | eqsstri 4017 | . 2 โข CPreHilOLD โ NrmCVec |
4 | 3 | sseli 3979 | 1 โข (๐ โ CPreHilOLD โ ๐ โ NrmCVec) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 = wceq 1542 โ wcel 2107 โwral 3062 โฉ cin 3948 ran crn 5678 โcfv 6544 (class class class)co 7409 {coprab 7410 1c1 11111 + caddc 11113 ยท cmul 11115 -cneg 11445 2c2 12267 โcexp 14027 NrmCVeccnv 29837 CPreHilOLDccphlo 30065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-ph 30066 |
This theorem is referenced by: phrel 30068 phnvi 30069 phop 30071 isph 30075 dipdi 30096 dipassr 30099 dipsubdir 30101 dipsubdi 30102 ajval 30114 minvecolem1 30127 minvecolem2 30128 minvecolem3 30129 minvecolem4a 30130 minvecolem4b 30131 minvecolem4 30133 minvecolem5 30134 minvecolem6 30135 minvecolem7 30136 |
Copyright terms: Public domain | W3C validator |