Theorem hhssmet

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

	Ref	Expression
Hypotheses	hhssims2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
	hhssims2.3	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
	hhssims2.2	⊢ 𝐻 ∈ Sℋ
Assertion	hhssmet	⊢ 𝐷 ∈ ( Met ‘ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		hhssims2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2		hhssims2.3	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3		hhssims2.2	⊢ 𝐻 ∈ Sℋ
4	1 3	hhssnv	⊢ 𝑊 ∈ NrmCVec
5	1 3	hhssba	⊢ 𝐻 = ( BaseSet ‘ 𝑊 )
6	5 2	imsmet	⊢ ( 𝑊 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝐻 ) )
7	4 6	ax-mp	⊢ 𝐷 ∈ ( Met ‘ 𝐻 )