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