Theorem imsdval2

Description: Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsdval2.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	imsdval2.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	imsdval2.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	imsdval2.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	imsdval2.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	imsdval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		imsdval2.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		imsdval2.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		imsdval2.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4		imsdval2.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
5		imsdval2.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
6		eqid	⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
7	1 6 4 5	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) )
8	1 2 3 6	nvmval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
9	8	fveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
10	7 9	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )