Theorem nvnd

Description: The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of Kreyszig p. 63. (Contributed by NM, 4-Dec-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvnd.1	|- X = ( BaseSet ` U )
	nvnd.5	|- Z = ( 0vec ` U )
	nvnd.6	|- N = ( normCV ` U )
	nvnd.8	|- D = ( IndMet ` U )
Assertion	nvnd	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( A D Z ) )

Proof

Step	Hyp	Ref	Expression
1		nvnd.1	|- X = ( BaseSet ` U )
2		nvnd.5	|- Z = ( 0vec ` U )
3		nvnd.6	|- N = ( normCV ` U )
4		nvnd.8	|- D = ( IndMet ` U )
5	1 2	nvzcl	|- ( U e. NrmCVec -> Z e. X )
6	5	adantr	|- ( ( U e. NrmCVec /\ A e. X ) -> Z e. X )
7		eqid	|- ( -v ` U ) = ( -v ` U )
8	1 7 3 4	imsdval	|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( A D Z ) = ( N ` ( A ( -v ` U ) Z ) ) )
9	6 8	mpd3an3	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A D Z ) = ( N ` ( A ( -v ` U ) Z ) ) )
10		eqid	|- ( +v ` U ) = ( +v ` U )
11		eqid	|- ( .sOLD ` U ) = ( .sOLD ` U )
12	1 10 11 7	nvmval	|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( A ( -v ` U ) Z ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) )
13	6 12	mpd3an3	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( -v ` U ) Z ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) )
14		neg1cn	|- -u 1 e. CC
15	11 2	nvsz	|- ( ( U e. NrmCVec /\ -u 1 e. CC ) -> ( -u 1 ( .sOLD ` U ) Z ) = Z )
16	14 15	mpan2	|- ( U e. NrmCVec -> ( -u 1 ( .sOLD ` U ) Z ) = Z )
17	16	oveq2d	|- ( U e. NrmCVec -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) Z ) )
18	17	adantr	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) Z ) )
19	1 10 2	nv0rid	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) Z ) = A )
20	13 18 19	3eqtrd	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( -v ` U ) Z ) = A )
21	20	fveq2d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( A ( -v ` U ) Z ) ) = ( N ` A ) )
22	9 21	eqtr2d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( A D Z ) )