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ℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) |
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ℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) |