Definition df-ims

Description: Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ims	⊢ IndMet = ( 𝑢 ∈ NrmCVec ↦ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cims	⊢ IndMet
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		cnmcv	⊢ normCV
4	1	cv	⊢ 𝑢
5	4 3	cfv	⊢ ( normCV ‘ 𝑢 )
6		cnsb	⊢ −𝑣
7	4 6	cfv	⊢ ( −𝑣 ‘ 𝑢 )
8	5 7	ccom	⊢ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) )
9	1 2 8	cmpt	⊢ ( 𝑢 ∈ NrmCVec ↦ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) )
10	0 9	wceq	⊢ IndMet = ( 𝑢 ∈ NrmCVec ↦ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) )