Description: Mapping for the norm function. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvf.1 | |- X = ( BaseSet ` U ) |
|
nvf.6 | |- N = ( normCV ` U ) |
||
Assertion | nvf | |- ( U e. NrmCVec -> N : X --> RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvf.1 | |- X = ( BaseSet ` U ) |
|
2 | nvf.6 | |- N = ( normCV ` U ) |
|
3 | eqid | |- ( +v ` U ) = ( +v ` U ) |
|
4 | eqid | |- ( .sOLD ` U ) = ( .sOLD ` U ) |
|
5 | eqid | |- ( 0vec ` U ) = ( 0vec ` U ) |
|
6 | 1 3 4 5 2 | nvi | |- ( U e. NrmCVec -> ( <. ( +v ` U ) , ( .sOLD ` U ) >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) |
7 | 6 | simp2d | |- ( U e. NrmCVec -> N : X --> RR ) |