Metamath Proof Explorer


Theorem nvf

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 )

Proof

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 )