Metamath Proof Explorer


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 ) )