This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → 𝐷 = ( 𝑁 ∘ 𝑀 ) )