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 ⊢ M = - v ⁡ U
imsval.6 ⊢ N = norm CV ⁡ U
imsval.8 ⊢ D = IndMet ⁡ U
Assertion imsval ⊢ U ∈ NrmCVec → D = N ∘ M

Proof

Step Hyp Ref Expression
1 imsval.3 ⊢ M = - v ⁡ U
2 imsval.6 ⊢ N = norm CV ⁡ U
3 imsval.8 ⊢ D = IndMet ⁡ U
4 fveq2 ⊢ u = U → norm CV ⁡ u = norm CV ⁡ U
5 fveq2 ⊢ u = U → - v ⁡ u = - v ⁡ U
6 4 5 coeq12d ⊢ u = U → norm CV ⁡ u ∘ - v ⁡ u = norm CV ⁡ U ∘ - v ⁡ U
7 df-ims ⊢ IndMet = u ∈ NrmCVec ⟼ norm CV ⁡ u ∘ - v ⁡ u
8 fvex ⊢ norm CV ⁡ U ∈ V
9 fvex ⊢ - v ⁡ U ∈ V
10 8 9 coex ⊢ norm CV ⁡ U ∘ - v ⁡ U ∈ V
11 6 7 10 fvmpt ⊢ U ∈ NrmCVec → IndMet ⁡ U = norm CV ⁡ U ∘ - v ⁡ U
12 2 1 coeq12i ⊢ N ∘ M = norm CV ⁡ U ∘ - v ⁡ U
13 11 3 12 3eqtr4g ⊢ U ∈ NrmCVec → D = N ∘ M