Theorem imsval

Description: Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsval.3	|- M = ( -v ` U )
	imsval.6	|- N = ( normCV ` U )
	imsval.8	|- D = ( IndMet ` U )
Assertion	imsval	|- ( U e. NrmCVec -> D = ( N o. M ) )

Proof

Step	Hyp	Ref	Expression
1		imsval.3	|- M = ( -v ` U )
2		imsval.6	|- N = ( normCV ` U )
3		imsval.8	|- D = ( IndMet ` U )
4		fveq2	|- ( u = U -> ( normCV ` u ) = ( normCV ` U ) )
5		fveq2	|- ( u = U -> ( -v ` u ) = ( -v ` U ) )
6	4 5	coeq12d	|- ( u = U -> ( ( normCV ` u ) o. ( -v ` u ) ) = ( ( normCV ` U ) o. ( -v ` U ) ) )
7		df-ims	|- IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )
8		fvex	|- ( normCV ` U ) e. _V
9		fvex	|- ( -v ` U ) e. _V
10	8 9	coex	|- ( ( normCV ` U ) o. ( -v ` U ) ) e. _V
11	6 7 10	fvmpt	|- ( U e. NrmCVec -> ( IndMet ` U ) = ( ( normCV ` U ) o. ( -v ` U ) ) )
12	2 1	coeq12i	|- ( N o. M ) = ( ( normCV ` U ) o. ( -v ` U ) )
13	11 3 12	3eqtr4g	|- ( U e. NrmCVec -> D = ( N o. M ) )