# 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}\left({U}\right)$
imsval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
imsval.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
Assertion imsval ${⊢}{U}\in \mathrm{NrmCVec}\to {D}={N}\circ {M}$

### Proof

Step Hyp Ref Expression
1 imsval.3 ${⊢}{M}={-}_{v}\left({U}\right)$
2 imsval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
3 imsval.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
4 fveq2 ${⊢}{u}={U}\to {norm}_{CV}\left({u}\right)={norm}_{CV}\left({U}\right)$
5 fveq2 ${⊢}{u}={U}\to {-}_{v}\left({u}\right)={-}_{v}\left({U}\right)$
6 4 5 coeq12d ${⊢}{u}={U}\to {norm}_{CV}\left({u}\right)\circ {-}_{v}\left({u}\right)={norm}_{CV}\left({U}\right)\circ {-}_{v}\left({U}\right)$
7 df-ims ${⊢}\mathrm{IndMet}=\left({u}\in \mathrm{NrmCVec}⟼{norm}_{CV}\left({u}\right)\circ {-}_{v}\left({u}\right)\right)$
8 fvex ${⊢}{norm}_{CV}\left({U}\right)\in \mathrm{V}$
9 fvex ${⊢}{-}_{v}\left({U}\right)\in \mathrm{V}$
10 8 9 coex ${⊢}{norm}_{CV}\left({U}\right)\circ {-}_{v}\left({U}\right)\in \mathrm{V}$
11 6 7 10 fvmpt ${⊢}{U}\in \mathrm{NrmCVec}\to \mathrm{IndMet}\left({U}\right)={norm}_{CV}\left({U}\right)\circ {-}_{v}\left({U}\right)$
12 2 1 coeq12i ${⊢}{N}\circ {M}={norm}_{CV}\left({U}\right)\circ {-}_{v}\left({U}\right)$
13 11 3 12 3eqtr4g ${⊢}{U}\in \mathrm{NrmCVec}\to {D}={N}\circ {M}$