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 )