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

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 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
sspims.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
sspims.c ⊢ 𝐶 = ( IndMet ‘ 𝑊 )
sspims.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspimsval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐶 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sspims.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2 sspims.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3 sspims.c ⊢ 𝐶 = ( IndMet ‘ 𝑊 )
4 sspims.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5 4 sspnv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
6 eqid ⊢ ( −𝑣 ‘ 𝑊 ) = ( −𝑣 ‘ 𝑊 )
7 1 6 nvmcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 )
8 7 3expb ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 )
9 5 8 sylan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 )
10 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
11 eqid ⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
12 1 10 11 4 sspnval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
13 12 3expa ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
14 9 13 syldan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
15 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
16 1 15 6 4 sspmval ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) = ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) )
17 16 fveq2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
18 14 17 eqtrd ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
19 1 6 11 3 imsdval ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 𝐶 𝐵 ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
20 19 3expb ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐶 𝐵 ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
21 5 20 sylan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐶 𝐵 ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑊 ) 𝐵 ) ) )
22 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
23 22 1 4 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
24 23 sseld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐴 ∈ 𝑌 → 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ) )
25 23 sseld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐵 ∈ 𝑌 → 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) )
26 24 25 anim12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) )
27 26 imp ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) )
28 22 15 10 2 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
29 28 3expb ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
30 29 adantlr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
31 27 30 syldan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
32 18 21 31 3eqtr4d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐶 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )