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→ACB=ADB

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⁡WB∈Y
8 7 3expb ⊢W∈NrmCVec∧A∈Y∧B∈Y→A-v⁡WB∈Y
9 5 8 sylan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A-v⁡WB∈Y
10 eqid ⊢normCV⁡U=normCV⁡U
11 eqid ⊢normCV⁡W=normCV⁡W
12 1 10 11 4 sspnval ⊢U∈NrmCVec∧W∈H∧A-v⁡WB∈Y→normCV⁡W⁡A-v⁡WB=normCV⁡U⁡A-v⁡WB
13 12 3expa ⊢U∈NrmCVec∧W∈H∧A-v⁡WB∈Y→normCV⁡W⁡A-v⁡WB=normCV⁡U⁡A-v⁡WB
14 9 13 syldan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→normCV⁡W⁡A-v⁡WB=normCV⁡U⁡A-v⁡WB
15 eqid ⊢-v⁡U=-v⁡U
16 1 15 6 4 sspmval ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A-v⁡WB=A-v⁡UB
17 16 fveq2d ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→normCV⁡U⁡A-v⁡WB=normCV⁡U⁡A-v⁡UB
18 14 17 eqtrd ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→normCV⁡W⁡A-v⁡WB=normCV⁡U⁡A-v⁡UB
19 1 6 11 3 imsdval ⊢W∈NrmCVec∧A∈Y∧B∈Y→ACB=normCV⁡W⁡A-v⁡WB
20 19 3expb ⊢W∈NrmCVec∧A∈Y∧B∈Y→ACB=normCV⁡W⁡A-v⁡WB
21 5 20 sylan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→ACB=normCV⁡W⁡A-v⁡WB
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→ADB=normCV⁡U⁡A-v⁡UB
29 28 3expb ⊢U∈NrmCVec∧A∈BaseSet⁡U∧B∈BaseSet⁡U→ADB=normCV⁡U⁡A-v⁡UB
30 29 adantlr ⊢U∈NrmCVec∧W∈H∧A∈BaseSet⁡U∧B∈BaseSet⁡U→ADB=normCV⁡U⁡A-v⁡UB
31 27 30 syldan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→ADB=normCV⁡U⁡A-v⁡UB
32 18 21 31 3eqtr4d ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→ACB=ADB