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

Metamath Proof Explorer

Theorem sspims

Description: The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspims.y ⊢ Y = BaseSet ⁡ W
sspims.d ⊢ D = IndMet ⁡ U
sspims.c ⊢ C = IndMet ⁡ W
sspims.h ⊢ H = SubSp ⁡ U
Assertion sspims ⊢ U ∈ NrmCVec ∧ W ∈ H → C = D ↾ Y × Y

Proof

Step Hyp Ref Expression
1 sspims.y ⊢ Y = BaseSet ⁡ W
2 sspims.d ⊢ D = IndMet ⁡ U
3 sspims.c ⊢ C = IndMet ⁡ W
4 sspims.h ⊢ H = SubSp ⁡ U
5 1 2 3 4 sspimsval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ x ∈ Y ∧ y ∈ Y → x C y = x D y
6 1 3 imsdf ⊢ W ∈ NrmCVec → C : Y × Y ⟶ ℝ
7 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
8 7 2 imsdf ⊢ U ∈ NrmCVec → D : BaseSet ⁡ U × BaseSet ⁡ U ⟶ ℝ
9 1 4 5 6 8 sspmlem ⊢ U ∈ NrmCVec ∧ W ∈ H → C = D ↾ Y × Y