# Metamath Proof Explorer

## Theorem nglmle

Description: If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value. (Contributed by NM, 25-Dec-2007) (Revised by AV, 16-Oct-2021)

Ref Expression
Hypotheses nglmle.1
`|- X = ( Base ` G )`
nglmle.2
`|- D = ( ( dist ` G ) |` ( X X. X ) )`
nglmle.3
`|- J = ( MetOpen ` D )`
nglmle.5
`|- N = ( norm ` G )`
nglmle.6
`|- ( ph -> G e. NrmGrp )`
nglmle.7
`|- ( ph -> F : NN --> X )`
nglmle.8
`|- ( ph -> F ( ~~>t ` J ) P )`
nglmle.9
`|- ( ph -> R e. RR* )`
nglmle.10
`|- ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) <_ R )`
Assertion nglmle
`|- ( ph -> ( N ` P ) <_ R )`

### Proof

Step Hyp Ref Expression
1 nglmle.1
` |-  X = ( Base ` G )`
2 nglmle.2
` |-  D = ( ( dist ` G ) |` ( X X. X ) )`
3 nglmle.3
` |-  J = ( MetOpen ` D )`
4 nglmle.5
` |-  N = ( norm ` G )`
5 nglmle.6
` |-  ( ph -> G e. NrmGrp )`
6 nglmle.7
` |-  ( ph -> F : NN --> X )`
7 nglmle.8
` |-  ( ph -> F ( ~~>t ` J ) P )`
8 nglmle.9
` |-  ( ph -> R e. RR* )`
9 nglmle.10
` |-  ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) <_ R )`
10 ngpgrp
` |-  ( G e. NrmGrp -> G e. Grp )`
11 5 10 syl
` |-  ( ph -> G e. Grp )`
12 ngpms
` |-  ( G e. NrmGrp -> G e. MetSp )`
13 5 12 syl
` |-  ( ph -> G e. MetSp )`
14 msxms
` |-  ( G e. MetSp -> G e. *MetSp )`
15 13 14 syl
` |-  ( ph -> G e. *MetSp )`
16 1 2 xmsxmet
` |-  ( G e. *MetSp -> D e. ( *Met ` X ) )`
17 15 16 syl
` |-  ( ph -> D e. ( *Met ` X ) )`
18 3 mopntopon
` |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )`
19 17 18 syl
` |-  ( ph -> J e. ( TopOn ` X ) )`
20 lmcl
` |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> P e. X )`
21 19 7 20 syl2anc
` |-  ( ph -> P e. X )`
22 eqid
` |-  ( 0g ` G ) = ( 0g ` G )`
23 eqid
` |-  ( dist ` G ) = ( dist ` G )`
24 4 1 22 23 2 nmval2
` |-  ( ( G e. Grp /\ P e. X ) -> ( N ` P ) = ( P D ( 0g ` G ) ) )`
25 11 21 24 syl2anc
` |-  ( ph -> ( N ` P ) = ( P D ( 0g ` G ) ) )`
26 1 22 grpidcl
` |-  ( G e. Grp -> ( 0g ` G ) e. X )`
27 11 26 syl
` |-  ( ph -> ( 0g ` G ) e. X )`
28 xmetsym
` |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( 0g ` G ) e. X ) -> ( P D ( 0g ` G ) ) = ( ( 0g ` G ) D P ) )`
29 17 21 27 28 syl3anc
` |-  ( ph -> ( P D ( 0g ` G ) ) = ( ( 0g ` G ) D P ) )`
30 25 29 eqtrd
` |-  ( ph -> ( N ` P ) = ( ( 0g ` G ) D P ) )`
31 nnuz
` |-  NN = ( ZZ>= ` 1 )`
32 1zzd
` |-  ( ph -> 1 e. ZZ )`
` |-  ( ( ph /\ k e. NN ) -> G e. Grp )`
34 6 ffvelrnda
` |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )`
35 4 1 22 23 2 nmval2
` |-  ( ( G e. Grp /\ ( F ` k ) e. X ) -> ( N ` ( F ` k ) ) = ( ( F ` k ) D ( 0g ` G ) ) )`
36 33 34 35 syl2anc
` |-  ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) = ( ( F ` k ) D ( 0g ` G ) ) )`
` |-  ( ( ph /\ k e. NN ) -> D e. ( *Met ` X ) )`
` |-  ( ( ph /\ k e. NN ) -> ( 0g ` G ) e. X )`
` |-  ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X /\ ( 0g ` G ) e. X ) -> ( ( F ` k ) D ( 0g ` G ) ) = ( ( 0g ` G ) D ( F ` k ) ) )`
` |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( 0g ` G ) ) = ( ( 0g ` G ) D ( F ` k ) ) )`
` |-  ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) = ( ( 0g ` G ) D ( F ` k ) ) )`
` |-  ( ( ph /\ k e. NN ) -> ( ( 0g ` G ) D ( F ` k ) ) <_ R )`
` |-  ( ph -> ( ( 0g ` G ) D P ) <_ R )`
` |-  ( ph -> ( N ` P ) <_ R )`