Theorem hhssims2

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	hhssims2	$$⊢D={\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\upharpoonright }_{\left(H\times 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		eqid	$$⊢{\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\upharpoonright }_{\left(H\times H\right)}={\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\upharpoonright }_{\left(H\times H\right)}$$
5	1 3 4	hhssims	$$⊢{\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\upharpoonright }_{\left(H\times H\right)}=\mathrm{IndMet}\left(W\right)$$
6	2 5	eqtr4i	$$⊢D={\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\upharpoonright }_{\left(H\times H\right)}$$