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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssims.2 ⊢ H ∈ S ℋ
hhssims.3 ⊢ D = norm ℎ ∘ - ℎ ↾ H × H
Assertion hhssims ⊢ D = IndMet ⁡ W

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssims.2 ⊢ H ∈ S ℋ
3 hhssims.3 ⊢ D = norm ℎ ∘ - ℎ ↾ H × H
4 1 2 hhssnv ⊢ W ∈ NrmCVec
5 1 2 hhssvs ⊢ - ℎ ↾ H × H = - v ⁡ W
6 1 hhssnm ⊢ norm ℎ ↾ H = norm CV ⁡ W
7 eqid ⊢ IndMet ⁡ W = IndMet ⁡ W
8 5 6 7 imsval ⊢ W ∈ NrmCVec → IndMet ⁡ W = norm ℎ ↾ H ∘ - ℎ ↾ H × H
9 4 8 ax-mp ⊢ IndMet ⁡ W = norm ℎ ↾ H ∘ - ℎ ↾ H × H
10 resco ⊢ norm ℎ ∘ - ℎ ↾ H × H = norm ℎ ∘ - ℎ ↾ H × H
11 1 2 hhssvsf ⊢ - ℎ ↾ H × H : H × H ⟶ H
12 frn ⊢ - ℎ ↾ H × H : H × H ⟶ H → ran ⁡ - ℎ ↾ H × H ⊆ H
13 11 12 ax-mp ⊢ ran ⁡ - ℎ ↾ H × H ⊆ H
14 cores ⊢ ran ⁡ - ℎ ↾ H × H ⊆ H → norm ℎ ↾ H ∘ - ℎ ↾ H × H = norm ℎ ∘ - ℎ ↾ H × H
15 13 14 ax-mp ⊢ norm ℎ ↾ H ∘ - ℎ ↾ H × H = norm ℎ ∘ - ℎ ↾ H × H
16 10 15 eqtr4i ⊢ norm ℎ ∘ - ℎ ↾ H × H = norm ℎ ↾ H ∘ - ℎ ↾ H × H
17 9 16 eqtr4i ⊢ IndMet ⁡ W = norm ℎ ∘ - ℎ ↾ H × H
18 3 17 eqtr4i ⊢ D = IndMet ⁡ W