Metamath Proof Explorer


Theorem hhssims2

Description: Induced metric 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 hhssims2 𝐷 = ( ( norm ∘ − ) ↾ ( 𝐻 × 𝐻 ) )

Proof

Step Hyp Ref Expression
1 hhssims2.1 𝑊 = ⟨ ⟨ ( + ↾ ( 𝐻 × 𝐻 ) ) , ( · ↾ ( ℂ × 𝐻 ) ) ⟩ , ( norm𝐻 ) ⟩
2 hhssims2.3 𝐷 = ( IndMet ‘ 𝑊 )
3 hhssims2.2 𝐻S
4 eqid ( ( norm ∘ − ) ↾ ( 𝐻 × 𝐻 ) ) = ( ( norm ∘ − ) ↾ ( 𝐻 × 𝐻 ) )
5 1 3 4 hhssims ( ( norm ∘ − ) ↾ ( 𝐻 × 𝐻 ) ) = ( IndMet ‘ 𝑊 )
6 2 5 eqtr4i 𝐷 = ( ( norm ∘ − ) ↾ ( 𝐻 × 𝐻 ) )