Theorem hhssmetdval

Description: Value of the distance function of the metric space 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	hhssmetdval	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )

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	1 3	hhssvs	⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 )
7	1	hhssnm	⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )
8	5 6 7 2	imsdval	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 𝐷 𝐵 ) = ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝐵 ) ) )
9	4 8	mp3an1	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 𝐷 𝐵 ) = ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝐵 ) ) )
10		ovres	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝐵 ) = ( 𝐴 −ℎ 𝐵 ) )
11	10	fveq2d	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝐵 ) ) = ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) )
12		shsubcl	⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐵 ) ∈ 𝐻 )
13	3 12	mp3an1	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐵 ) ∈ 𝐻 )
14		fvres	⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ 𝐻 → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )
15	13 14	syl	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )
16	9 11 15	3eqtrd	⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )