Theorem imsdval

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsdval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	imsdval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	imsdval.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	imsdval.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imsdval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		imsdval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		imsdval.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		imsdval.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
5	2 3 4	imsval	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( 𝑁 ∘ 𝑀 ) )
6	5	3ad2ant1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐷 = ( 𝑁 ∘ 𝑀 ) )
7	6	fveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑁 ∘ 𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8	1 2	nvmf	⊢ ( 𝑈 ∈ NrmCVec → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9		opelxpi	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
10		fvco3	⊢ ( ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ 𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
11	8 9 10	syl2an	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑁 ∘ 𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
12	11	3impb	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ∘ 𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
13	7 12	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
14		df-ov	⊢ ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
15		df-ov	⊢ ( 𝐴 𝑀 𝐵 ) = ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
16	15	fveq2i	⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
17	13 14 16	3eqtr4g	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )