Theorem hilims

Description: Hilbert space distance metric. (Contributed by NM, 13-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilims.1	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
	hilims.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
	hilims.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	hilims.5	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	hilims.8	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	hilims.9	$$⊢U\in \mathrm{NrmCVec}$$
Assertion	hilims	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		hilims.1	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
2		hilims.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
3		hilims.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		hilims.5	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
5		hilims.8	$$⊢D=\mathrm{IndMet}\left(U\right)$$
6		hilims.9	$$⊢U\in \mathrm{NrmCVec}$$
7	1 2 3 4 6	hilhhi	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
8	7 5	hhims2	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$