Metamath Proof Explorer

Theorem ncvspds

Description: Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised by AV, 13-Oct-2021)

Ref Expression
Hypotheses ncvspds.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
ncvspds.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
ncvspds.p
ncvspds.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
ncvspds.s
Assertion ncvspds

Proof

Step Hyp Ref Expression
1 ncvspds.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
2 ncvspds.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
3 ncvspds.p
4 ncvspds.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
5 ncvspds.s
6 elin ${⊢}{G}\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)↔\left({G}\in \mathrm{NrmVec}\wedge {G}\in \mathrm{ℂVec}\right)$
7 nvcnlm ${⊢}{G}\in \mathrm{NrmVec}\to {G}\in \mathrm{NrmMod}$
8 nlmngp ${⊢}{G}\in \mathrm{NrmMod}\to {G}\in \mathrm{NrmGrp}$
9 7 8 syl ${⊢}{G}\in \mathrm{NrmVec}\to {G}\in \mathrm{NrmGrp}$
10 9 adantr ${⊢}\left({G}\in \mathrm{NrmVec}\wedge {G}\in \mathrm{ℂVec}\right)\to {G}\in \mathrm{NrmGrp}$
11 6 10 sylbi ${⊢}{G}\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)\to {G}\in \mathrm{NrmGrp}$
12 eqid ${⊢}{-}_{{G}}={-}_{{G}}$
13 1 2 12 4 ngpds ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={N}\left({A}{-}_{{G}}{B}\right)$
14 11 13 syl3an1 ${⊢}\left({G}\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={N}\left({A}{-}_{{G}}{B}\right)$
15 id ${⊢}{G}\in \mathrm{ℂVec}\to {G}\in \mathrm{ℂVec}$
16 15 cvsclm ${⊢}{G}\in \mathrm{ℂVec}\to {G}\in \mathrm{CMod}$
17 6 16 simplbiim ${⊢}{G}\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)\to {G}\in \mathrm{CMod}$
18 eqid ${⊢}\mathrm{Scalar}\left({G}\right)=\mathrm{Scalar}\left({G}\right)$
19 2 3 12 18 5 clmvsubval
20 17 19 syl3an1
21 20 fveq2d
22 14 21 eqtrd