This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )