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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐶 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )