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 )
33 11 adantr 
 |-  ( ( ph /\ k e. NN ) -> G e. Grp )
34 6 ffvelcdmda 
 |-  ( ( 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 ) ) )
37 17 adantr 
 |-  ( ( ph /\ k e. NN ) -> D e. ( *Met ` X ) )
38 27 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( 0g ` G ) e. X )
39 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X /\ ( 0g ` G ) e. X ) -> ( ( F ` k ) D ( 0g ` G ) ) = ( ( 0g ` G ) D ( F ` k ) ) )
40 37 34 38 39 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( 0g ` G ) ) = ( ( 0g ` G ) D ( F ` k ) ) )
41 36 40 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) = ( ( 0g ` G ) D ( F ` k ) ) )
42 41 9 eqbrtrrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( 0g ` G ) D ( F ` k ) ) <_ R )
43 31 3 17 32 7 27 8 42 lmle 
 |-  ( ph -> ( ( 0g ` G ) D P ) <_ R )
44 30 43 eqbrtrd 
 |-  ( ph -> ( N ` P ) <_ R )