# Metamath Proof Explorer

## Theorem tngnm

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngnm.t ${⊢}{T}={G}\mathrm{toNrmGrp}{N}$
tngnm.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
tngnm.a ${⊢}{A}\in \mathrm{V}$
Assertion tngnm ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}=\mathrm{norm}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 tngnm.t ${⊢}{T}={G}\mathrm{toNrmGrp}{N}$
2 tngnm.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
3 tngnm.a ${⊢}{A}\in \mathrm{V}$
4 simpr ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}:{X}⟶{A}$
5 4 feqmptd ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}=\left({x}\in {X}⟼{N}\left({x}\right)\right)$
6 eqid ${⊢}{-}_{{G}}={-}_{{G}}$
7 2 6 grpsubf ${⊢}{G}\in \mathrm{Grp}\to {-}_{{G}}:{X}×{X}⟶{X}$
8 7 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {-}_{{G}}:{X}×{X}⟶{X}$
9 simpr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {x}\in {X}$
10 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
11 2 10 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {X}$
12 11 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {0}_{{G}}\in {X}$
13 9 12 opelxpd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to ⟨{x},{0}_{{G}}⟩\in \left({X}×{X}\right)$
14 fvco3 ${⊢}\left({-}_{{G}}:{X}×{X}⟶{X}\wedge ⟨{x},{0}_{{G}}⟩\in \left({X}×{X}\right)\right)\to \left({N}\circ {-}_{{G}}\right)\left(⟨{x},{0}_{{G}}⟩\right)={N}\left({-}_{{G}}\left(⟨{x},{0}_{{G}}⟩\right)\right)$
15 8 13 14 syl2anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to \left({N}\circ {-}_{{G}}\right)\left(⟨{x},{0}_{{G}}⟩\right)={N}\left({-}_{{G}}\left(⟨{x},{0}_{{G}}⟩\right)\right)$
16 df-ov ${⊢}{x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}=\left({N}\circ {-}_{{G}}\right)\left(⟨{x},{0}_{{G}}⟩\right)$
17 df-ov ${⊢}{x}{-}_{{G}}{0}_{{G}}={-}_{{G}}\left(⟨{x},{0}_{{G}}⟩\right)$
18 17 fveq2i ${⊢}{N}\left({x}{-}_{{G}}{0}_{{G}}\right)={N}\left({-}_{{G}}\left(⟨{x},{0}_{{G}}⟩\right)\right)$
19 15 16 18 3eqtr4g ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}={N}\left({x}{-}_{{G}}{0}_{{G}}\right)$
20 2 10 6 grpsubid1 ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in {X}\right)\to {x}{-}_{{G}}{0}_{{G}}={x}$
21 20 adantlr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {x}{-}_{{G}}{0}_{{G}}={x}$
22 21 fveq2d ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {N}\left({x}{-}_{{G}}{0}_{{G}}\right)={N}\left({x}\right)$
23 19 22 eqtr2d ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\wedge {x}\in {X}\right)\to {N}\left({x}\right)={x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}$
24 23 mpteq2dva ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to \left({x}\in {X}⟼{N}\left({x}\right)\right)=\left({x}\in {X}⟼{x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}\right)$
25 2 fvexi ${⊢}{X}\in \mathrm{V}$
26 fex2 ${⊢}\left({N}:{X}⟶{A}\wedge {X}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {N}\in \mathrm{V}$
27 25 3 26 mp3an23 ${⊢}{N}:{X}⟶{A}\to {N}\in \mathrm{V}$
28 27 adantl ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}\in \mathrm{V}$
29 1 2 tngbas ${⊢}{N}\in \mathrm{V}\to {X}={\mathrm{Base}}_{{T}}$
30 28 29 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {X}={\mathrm{Base}}_{{T}}$
31 1 6 tngds ${⊢}{N}\in \mathrm{V}\to {N}\circ {-}_{{G}}=\mathrm{dist}\left({T}\right)$
32 28 31 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}\circ {-}_{{G}}=\mathrm{dist}\left({T}\right)$
33 eqidd ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {x}={x}$
34 1 10 tng0 ${⊢}{N}\in \mathrm{V}\to {0}_{{G}}={0}_{{T}}$
35 28 34 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {0}_{{G}}={0}_{{T}}$
36 32 33 35 oveq123d ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}={x}\mathrm{dist}\left({T}\right){0}_{{T}}$
37 30 36 mpteq12dv ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to \left({x}\in {X}⟼{x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}\right)=\left({x}\in {\mathrm{Base}}_{{T}}⟼{x}\mathrm{dist}\left({T}\right){0}_{{T}}\right)$
38 eqid ${⊢}\mathrm{norm}\left({T}\right)=\mathrm{norm}\left({T}\right)$
39 eqid ${⊢}{\mathrm{Base}}_{{T}}={\mathrm{Base}}_{{T}}$
40 eqid ${⊢}{0}_{{T}}={0}_{{T}}$
41 eqid ${⊢}\mathrm{dist}\left({T}\right)=\mathrm{dist}\left({T}\right)$
42 38 39 40 41 nmfval ${⊢}\mathrm{norm}\left({T}\right)=\left({x}\in {\mathrm{Base}}_{{T}}⟼{x}\mathrm{dist}\left({T}\right){0}_{{T}}\right)$
43 37 42 syl6eqr ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to \left({x}\in {X}⟼{x}\left({N}\circ {-}_{{G}}\right){0}_{{G}}\right)=\mathrm{norm}\left({T}\right)$
44 5 24 43 3eqtrd ${⊢}\left({G}\in \mathrm{Grp}\wedge {N}:{X}⟶{A}\right)\to {N}=\mathrm{norm}\left({T}\right)$