Description: The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008) (Revised by AV, 9-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cnrnvc.c | |- C = ( ringLMod ` CCfld ) |
|
| Assertion | cnnm | |- ( norm ` C ) = abs |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnrnvc.c | |- C = ( ringLMod ` CCfld ) |
|
| 2 | rlmnm | |- ( norm ` CCfld ) = ( norm ` ( ringLMod ` CCfld ) ) |
|
| 3 | cnfldnm | |- abs = ( norm ` CCfld ) |
|
| 4 | 1 | fveq2i | |- ( norm ` C ) = ( norm ` ( ringLMod ` CCfld ) ) |
| 5 | 2 3 4 | 3eqtr4ri | |- ( norm ` C ) = abs |