Description: The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cnnvnm.6 | |- U = <. <. + , x. >. , abs >. |
|
| Assertion | cnnvnm | |- abs = ( normCV ` U ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnnvnm.6 | |- U = <. <. + , x. >. , abs >. |
|
| 2 | eqid | |- ( normCV ` U ) = ( normCV ` U ) |
|
| 3 | 2 | nmcvfval | |- ( normCV ` U ) = ( 2nd ` U ) |
| 4 | 1 | fveq2i | |- ( 2nd ` U ) = ( 2nd ` <. <. + , x. >. , abs >. ) |
| 5 | opex | |- <. + , x. >. e. _V |
|
| 6 | absf | |- abs : CC --> RR |
|
| 7 | cnex | |- CC e. _V |
|
| 8 | fex | |- ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V ) |
|
| 9 | 6 7 8 | mp2an | |- abs e. _V |
| 10 | 5 9 | op2nd | |- ( 2nd ` <. <. + , x. >. , abs >. ) = abs |
| 11 | 3 4 10 | 3eqtrri | |- abs = ( normCV ` U ) |