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

Metamath Proof Explorer

Theorem hhssims

Description: Induced metric of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsssh2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
hhssims.2 ⊢ 𝐻 ∈ Sℋ
hhssims.3 ⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
Assertion hhssims 𝐷 = ( IndMet ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 hhssims.2 ⊢ 𝐻 ∈ Sℋ
3 hhssims.3 ⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
4 1 2 hhssnv ⊢ 𝑊 ∈ NrmCVec
5 1 2 hhssvs ⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 )
6 1 hhssnm ⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )
7 eqid ⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
8 5 6 7 imsval ⊢ ( 𝑊 ∈ NrmCVec → ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) )
9 4 8 ax-mp ⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
10 resco ⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
11 1 2 hhssvsf ⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻
12 frn ⊢ ( ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 → ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 )
13 11 12 ax-mp ⊢ ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻
14 cores ⊢ ( ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 → ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) )
15 13 14 ax-mp ⊢ ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
16 10 15 eqtr4i ⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
17 9 16 eqtr4i ⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
18 3 17 eqtr4i ⊢ 𝐷 = ( IndMet ‘ 𝑊 )