Theorem imsdval

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsdval.1	|- X = ( BaseSet ` U )
	imsdval.3	|- M = ( -v ` U )
	imsdval.6	|- N = ( normCV ` U )
	imsdval.8	|- D = ( IndMet ` U )
Assertion	imsdval	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A M B ) ) )

Proof

Step	Hyp	Ref	Expression
1		imsdval.1	|- X = ( BaseSet ` U )
2		imsdval.3	|- M = ( -v ` U )
3		imsdval.6	|- N = ( normCV ` U )
4		imsdval.8	|- D = ( IndMet ` U )
5	2 3 4	imsval	|- ( U e. NrmCVec -> D = ( N o. M ) )
6	5	3ad2ant1	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> D = ( N o. M ) )
7	6	fveq1d	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( D ` <. A , B >. ) = ( ( N o. M ) ` <. A , B >. ) )
8	1 2	nvmf	|- ( U e. NrmCVec -> M : ( X X. X ) --> X )
9		opelxpi	|- ( ( A e. X /\ B e. X ) -> <. A , B >. e. ( X X. X ) )
10		fvco3	|- ( ( M : ( X X. X ) --> X /\ <. A , B >. e. ( X X. X ) ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
11	8 9 10	syl2an	|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
12	11	3impb	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
13	7 12	eqtrd	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( D ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
14		df-ov	|- ( A D B ) = ( D ` <. A , B >. )
15		df-ov	|- ( A M B ) = ( M ` <. A , B >. )
16	15	fveq2i	|- ( N ` ( A M B ) ) = ( N ` ( M ` <. A , B >. ) )
17	13 14 16	3eqtr4g	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A M B ) ) )