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 ‘ 𝑊 )