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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssims2.3 ⊢ D = IndMet ⁡ W
hhssims2.2 ⊢ H ∈ S ℋ
Assertion hhssmetdval ⊢ A ∈ H ∧ B ∈ H → A D B = norm ℎ ⁡ A - ℎ B

Proof

Step Hyp Ref Expression
1 hhssims2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssims2.3 ⊢ D = IndMet ⁡ W
3 hhssims2.2 ⊢ H ∈ S ℋ
4 1 3 hhssnv ⊢ W ∈ NrmCVec
5 1 3 hhssba ⊢ H = BaseSet ⁡ W
6 1 3 hhssvs ⊢ - ℎ ↾ H × H = - v ⁡ W
7 1 hhssnm ⊢ norm ℎ ↾ H = norm CV ⁡ W
8 5 6 7 2 imsdval ⊢ W ∈ NrmCVec ∧ A ∈ H ∧ B ∈ H → A D B = norm ℎ ↾ H ⁡ A - ℎ ↾ H × H B
9 4 8 mp3an1 ⊢ A ∈ H ∧ B ∈ H → A D B = norm ℎ ↾ H ⁡ A - ℎ ↾ H × H B
10 ovres ⊢ A ∈ H ∧ B ∈ H → A - ℎ ↾ H × H B = A - ℎ B
11 10 fveq2d ⊢ A ∈ H ∧ B ∈ H → norm ℎ ↾ H ⁡ A - ℎ ↾ H × H B = norm ℎ ↾ H ⁡ A - ℎ B
12 shsubcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A - ℎ B ∈ H
13 3 12 mp3an1 ⊢ A ∈ H ∧ B ∈ H → A - ℎ B ∈ H
14 fvres ⊢ A - ℎ B ∈ H → norm ℎ ↾ H ⁡ A - ℎ B = norm ℎ ⁡ A - ℎ B
15 13 14 syl ⊢ A ∈ H ∧ B ∈ H → norm ℎ ↾ H ⁡ A - ℎ B = norm ℎ ⁡ A - ℎ B
16 9 11 15 3eqtrd ⊢ A ∈ H ∧ B ∈ H → A D B = norm ℎ ⁡ A - ℎ B