# Metamath Proof Explorer

## Theorem isngp2

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses isngp.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
isngp.z
isngp.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
isngp2.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
isngp2.e ${⊢}{E}={{D}↾}_{\left({X}×{X}\right)}$
Assertion isngp2

### Proof

Step Hyp Ref Expression
1 isngp.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
2 isngp.z
3 isngp.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
4 isngp2.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
5 isngp2.e ${⊢}{E}={{D}↾}_{\left({X}×{X}\right)}$
6 1 2 3 isngp
7 resss ${⊢}{{D}↾}_{\left({X}×{X}\right)}\subseteq {D}$
8 5 7 eqsstri ${⊢}{E}\subseteq {D}$
9 sseq1
10 8 9 mpbiri
11 3 reseq1i ${⊢}{{D}↾}_{\left({X}×{X}\right)}={\mathrm{dist}\left({G}\right)↾}_{\left({X}×{X}\right)}$
12 5 11 eqtri ${⊢}{E}={\mathrm{dist}\left({G}\right)↾}_{\left({X}×{X}\right)}$
13 4 12 msmet ${⊢}{G}\in \mathrm{MetSp}\to {E}\in \mathrm{Met}\left({X}\right)$
14 1 4 3 5 nmf2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {E}\in \mathrm{Met}\left({X}\right)\right)\to {N}:{X}⟶ℝ$
15 13 14 sylan2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{MetSp}\right)\to {N}:{X}⟶ℝ$
16 4 2 grpsubf
18 fco
19 15 17 18 syl2an2r
20 19 fdmd
21 20 reseq2d
22 4 12 msf ${⊢}{G}\in \mathrm{MetSp}\to {E}:{X}×{X}⟶ℝ$
24 23 ffund
25 simpr
26 ssv ${⊢}ℝ\subseteq \mathrm{V}$
27 fss
28 19 26 27 sylancl
29 fssxp
30 28 29 syl
31 25 30 ssind
32 df-res ${⊢}{{D}↾}_{\left({X}×{X}\right)}={D}\cap \left(\left({X}×{X}\right)×\mathrm{V}\right)$
33 5 32 eqtri ${⊢}{E}={D}\cap \left(\left({X}×{X}\right)×\mathrm{V}\right)$
34 31 33 sseqtrrdi
35 funssres
36 24 34 35 syl2anc
37 ffn ${⊢}{E}:{X}×{X}⟶ℝ\to {E}Fn\left({X}×{X}\right)$
38 fnresdm ${⊢}{E}Fn\left({X}×{X}\right)\to {{E}↾}_{\left({X}×{X}\right)}={E}$
39 23 37 38 3syl
40 21 36 39 3eqtr3d
41 40 ex
42 10 41 impbid2
43 42 pm5.32i
44 df-3an
45 df-3an
46 43 44 45 3bitr4i
47 6 46 bitr4i