Theorem hhssmet

Description: Induced metric of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhssims2.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
	hhssims2.3	$$⊢D=\mathrm{IndMet}\left(W\right)$$
	hhssims2.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	hhssmet	$$⊢D\in \mathrm{Met}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhssims2.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
2		hhssims2.3	$$⊢D=\mathrm{IndMet}\left(W\right)$$
3		hhssims2.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
4	1 3	hhssnv	$$⊢W\in \mathrm{NrmCVec}$$
5	1 3	hhssba	$$⊢H=\mathrm{BaseSet}\left(W\right)$$
6	5 2	imsmet	$$⊢W\in \mathrm{NrmCVec}\to D\in \mathrm{Met}\left(H\right)$$
7	4 6	ax-mp	$$⊢D\in \mathrm{Met}\left(H\right)$$