Theorem imsval

Description: Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	imsval.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	imsval.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	imsval	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( 𝑁 ∘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		imsval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
2		imsval.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
3		imsval.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
4		fveq2	⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) )
5		fveq2	⊢ ( 𝑢 = 𝑈 → ( −𝑣 ‘ 𝑢 ) = ( −𝑣 ‘ 𝑈 ) )
6	4 5	coeq12d	⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) )
7		df-ims	⊢ IndMet = ( 𝑢 ∈ NrmCVec ↦ ( ( normCV ‘ 𝑢 ) ∘ ( −𝑣 ‘ 𝑢 ) ) )
8		fvex	⊢ ( normCV ‘ 𝑈 ) ∈ V
9		fvex	⊢ ( −𝑣 ‘ 𝑈 ) ∈ V
10	8 9	coex	⊢ ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) ∈ V
11	6 7 10	fvmpt	⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) )
12	2 1	coeq12i	⊢ ( 𝑁 ∘ 𝑀 ) = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) )
13	11 3 12	3eqtr4g	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( 𝑁 ∘ 𝑀 ) )