Description: A normed complex vector space is an ordered pair of a vector space and a norm operation. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nvop2.1 | |- W = ( 1st ` U ) |
|
| nvop2.6 | |- N = ( normCV ` U ) |
||
| Assertion | nvop2 | |- ( U e. NrmCVec -> U = <. W , N >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvop2.1 | |- W = ( 1st ` U ) |
|
| 2 | nvop2.6 | |- N = ( normCV ` U ) |
|
| 3 | nvrel | |- Rel NrmCVec |
|
| 4 | 1st2nd | |- ( ( Rel NrmCVec /\ U e. NrmCVec ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. ) |
|
| 5 | 3 4 | mpan | |- ( U e. NrmCVec -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. ) |
| 6 | 2 | nmcvfval | |- N = ( 2nd ` U ) |
| 7 | 1 6 | opeq12i | |- <. W , N >. = <. ( 1st ` U ) , ( 2nd ` U ) >. |
| 8 | 5 7 | eqtr4di | |- ( U e. NrmCVec -> U = <. W , N >. ) |