# Metamath Proof Explorer

## Theorem imsdval

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses imsdval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
imsdval.3 ${⊢}{M}={-}_{v}\left({U}\right)$
imsdval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
imsdval.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
Assertion imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={N}\left({A}{M}{B}\right)$

### Proof

Step Hyp Ref Expression
1 imsdval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 imsdval.3 ${⊢}{M}={-}_{v}\left({U}\right)$
3 imsdval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
4 imsdval.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
5 2 3 4 imsval ${⊢}{U}\in \mathrm{NrmCVec}\to {D}={N}\circ {M}$
6 5 3ad2ant1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {D}={N}\circ {M}$
7 6 fveq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {D}\left(⟨{A},{B}⟩\right)=\left({N}\circ {M}\right)\left(⟨{A},{B}⟩\right)$
8 1 2 nvmf ${⊢}{U}\in \mathrm{NrmCVec}\to {M}:{X}×{X}⟶{X}$
9 opelxpi ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to ⟨{A},{B}⟩\in \left({X}×{X}\right)$
10 fvco3 ${⊢}\left({M}:{X}×{X}⟶{X}\wedge ⟨{A},{B}⟩\in \left({X}×{X}\right)\right)\to \left({N}\circ {M}\right)\left(⟨{A},{B}⟩\right)={N}\left({M}\left(⟨{A},{B}⟩\right)\right)$
11 8 9 10 syl2an ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({N}\circ {M}\right)\left(⟨{A},{B}⟩\right)={N}\left({M}\left(⟨{A},{B}⟩\right)\right)$
12 11 3impb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({N}\circ {M}\right)\left(⟨{A},{B}⟩\right)={N}\left({M}\left(⟨{A},{B}⟩\right)\right)$
13 7 12 eqtrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {D}\left(⟨{A},{B}⟩\right)={N}\left({M}\left(⟨{A},{B}⟩\right)\right)$
14 df-ov ${⊢}{A}{D}{B}={D}\left(⟨{A},{B}⟩\right)$
15 df-ov ${⊢}{A}{M}{B}={M}\left(⟨{A},{B}⟩\right)$
16 15 fveq2i ${⊢}{N}\left({A}{M}{B}\right)={N}\left({M}\left(⟨{A},{B}⟩\right)\right)$
17 13 14 16 3eqtr4g ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={N}\left({A}{M}{B}\right)$