Theorem hhims

Description: The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnv.1	|- U = <. <. +h , .h >. , normh >.
	hhims.2	|- D = ( normh o. -h )
Assertion	hhims	|- D = ( IndMet ` U )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	|- U = <. <. +h , .h >. , normh >.
2		hhims.2	|- D = ( normh o. -h )
3	1	hhnv	|- U e. NrmCVec
4	1	hhvs	|- -h = ( -v ` U )
5	1	hhnm	|- normh = ( normCV ` U )
6		eqid	|- ( IndMet ` U ) = ( IndMet ` U )
7	4 5 6	imsval	|- ( U e. NrmCVec -> ( IndMet ` U ) = ( normh o. -h ) )
8	3 7	ax-mp	|- ( IndMet ` U ) = ( normh o. -h )
9	2 8	eqtr4i	|- D = ( IndMet ` U )