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 𝑌 = ( BaseSet ‘ 𝑊 )
sspims.d 𝐷 = ( IndMet ‘ 𝑈 )
sspims.c 𝐶 = ( IndMet ‘ 𝑊 )
sspims.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspims ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝐶 = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 sspims.y 𝑌 = ( BaseSet ‘ 𝑊 )
2 sspims.d 𝐷 = ( IndMet ‘ 𝑈 )
3 sspims.c 𝐶 = ( IndMet ‘ 𝑊 )
4 sspims.h 𝐻 = ( SubSp ‘ 𝑈 )
5 1 2 3 4 sspimsval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑌𝑦𝑌 ) ) → ( 𝑥 𝐶 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
6 1 3 imsdf ( 𝑊 ∈ NrmCVec → 𝐶 : ( 𝑌 × 𝑌 ) ⟶ ℝ )
7 eqid ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
8 7 2 imsdf ( 𝑈 ∈ NrmCVec → 𝐷 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ℝ )
9 1 4 5 6 8 sspmlem ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝐶 = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )