This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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