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=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhims.2	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
Assertion	hhims	$$⊢D=\mathrm{IndMet}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhims.2	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
3	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
4	1	hhvs	$$⊢{-}_{ℎ}={-}_v\left(U\right)$$
5	1	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$
6		eqid	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{IndMet}\left(U\right)$$
7	4 5 6	imsval	$$⊢U\in \mathrm{NrmCVec}\to \mathrm{IndMet}\left(U\right)={norm}_{ℎ}\circ {-}_{ℎ}$$
8	3 7	ax-mp	$$⊢\mathrm{IndMet}\left(U\right)={norm}_{ℎ}\circ {-}_{ℎ}$$
9	2 8	eqtr4i	$$⊢D=\mathrm{IndMet}\left(U\right)$$