Metamath Proof Explorer

Theorem sspimsval

Description: The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspims.y ⊢ Y = BaseSet ⁡ W
sspims.d ⊢ D = IndMet ⁡ U
sspims.c ⊢ C = IndMet ⁡ W
sspims.h ⊢ H = SubSp ⁡ U
Assertion sspimsval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A C B = A D B

Proof

Step Hyp Ref Expression
1 sspims.y ⊢ Y = BaseSet ⁡ W
2 sspims.d ⊢ D = IndMet ⁡ U
3 sspims.c ⊢ C = IndMet ⁡ W
4 sspims.h ⊢ H = SubSp ⁡ U
5 4 sspnv ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec
6 eqid ⊢ - v ⁡ W = - v ⁡ W
7 1 6 nvmcl ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A - v ⁡ W B ∈ Y
8 7 3expb ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A - v ⁡ W B ∈ Y
9 5 8 sylan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A - v ⁡ W B ∈ Y
10 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
11 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
12 1 10 11 4 sspnval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A - v ⁡ W B ∈ Y → norm CV ⁡ W ⁡ A - v ⁡ W B = norm CV ⁡ U ⁡ A - v ⁡ W B
13 12 3expa ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A - v ⁡ W B ∈ Y → norm CV ⁡ W ⁡ A - v ⁡ W B = norm CV ⁡ U ⁡ A - v ⁡ W B
14 9 13 syldan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → norm CV ⁡ W ⁡ A - v ⁡ W B = norm CV ⁡ U ⁡ A - v ⁡ W B
15 eqid ⊢ - v ⁡ U = - v ⁡ U
16 1 15 6 4 sspmval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A - v ⁡ W B = A - v ⁡ U B
17 16 fveq2d ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → norm CV ⁡ U ⁡ A - v ⁡ W B = norm CV ⁡ U ⁡ A - v ⁡ U B
18 14 17 eqtrd ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → norm CV ⁡ W ⁡ A - v ⁡ W B = norm CV ⁡ U ⁡ A - v ⁡ U B
19 1 6 11 3 imsdval ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A C B = norm CV ⁡ W ⁡ A - v ⁡ W B
20 19 3expb ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A C B = norm CV ⁡ W ⁡ A - v ⁡ W B
21 5 20 sylan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A C B = norm CV ⁡ W ⁡ A - v ⁡ W B
22 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
23 22 1 4 sspba ⊢ U ∈ NrmCVec ∧ W ∈ H → Y ⊆ BaseSet ⁡ U
24 23 sseld ⊢ U ∈ NrmCVec ∧ W ∈ H → A ∈ Y → A ∈ BaseSet ⁡ U
25 23 sseld ⊢ U ∈ NrmCVec ∧ W ∈ H → B ∈ Y → B ∈ BaseSet ⁡ U
26 24 25 anim12d ⊢ U ∈ NrmCVec ∧ W ∈ H → A ∈ Y ∧ B ∈ Y → A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U
27 26 imp ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U
28 22 15 10 2 imsdval ⊢ U ∈ NrmCVec ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A D B = norm CV ⁡ U ⁡ A - v ⁡ U B
29 28 3expb ⊢ U ∈ NrmCVec ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A D B = norm CV ⁡ U ⁡ A - v ⁡ U B
30 29 adantlr ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A D B = norm CV ⁡ U ⁡ A - v ⁡ U B
31 27 30 syldan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A D B = norm CV ⁡ U ⁡ A - v ⁡ U B
32 18 21 31 3eqtr4d ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A C B = A D B