Theorem hhssims2

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	hhssims2	⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		hhssims2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2		hhssims2.3	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3		hhssims2.2	⊢ 𝐻 ∈ Sℋ
4		eqid	⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
5	1 3 4	hhssims	⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( IndMet ‘ 𝑊 )
6	2 5	eqtr4i	⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )