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}={\mathrm{Base}}_{{G}}$
nglmle.2 ${⊢}{D}={\mathrm{dist}\left({G}\right)↾}_{\left({X}×{X}\right)}$
nglmle.3 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
nglmle.5 ${⊢}{N}=\mathrm{norm}\left({G}\right)$
nglmle.6 ${⊢}{\phi }\to {G}\in \mathrm{NrmGrp}$
nglmle.7 ${⊢}{\phi }\to {F}:ℕ⟶{X}$
nglmle.8
nglmle.9 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
nglmle.10 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {N}\left({F}\left({k}\right)\right)\le {R}$
Assertion nglmle ${⊢}{\phi }\to {N}\left({P}\right)\le {R}$

Proof

Step Hyp Ref Expression
1 nglmle.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 nglmle.2 ${⊢}{D}={\mathrm{dist}\left({G}\right)↾}_{\left({X}×{X}\right)}$
3 nglmle.3 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
4 nglmle.5 ${⊢}{N}=\mathrm{norm}\left({G}\right)$
5 nglmle.6 ${⊢}{\phi }\to {G}\in \mathrm{NrmGrp}$
6 nglmle.7 ${⊢}{\phi }\to {F}:ℕ⟶{X}$
7 nglmle.8
8 nglmle.9 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
9 nglmle.10 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {N}\left({F}\left({k}\right)\right)\le {R}$
10 ngpgrp ${⊢}{G}\in \mathrm{NrmGrp}\to {G}\in \mathrm{Grp}$
11 5 10 syl ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
12 ngpms ${⊢}{G}\in \mathrm{NrmGrp}\to {G}\in \mathrm{MetSp}$
13 5 12 syl ${⊢}{\phi }\to {G}\in \mathrm{MetSp}$
14 msxms ${⊢}{G}\in \mathrm{MetSp}\to {G}\in \mathrm{\infty MetSp}$
15 13 14 syl ${⊢}{\phi }\to {G}\in \mathrm{\infty MetSp}$
16 1 2 xmsxmet ${⊢}{G}\in \mathrm{\infty MetSp}\to {D}\in \mathrm{\infty Met}\left({X}\right)$
17 15 16 syl ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
18 3 mopntopon ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
19 17 18 syl ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
20 lmcl
21 19 7 20 syl2anc ${⊢}{\phi }\to {P}\in {X}$
22 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
23 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
24 4 1 22 23 2 nmval2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {P}\in {X}\right)\to {N}\left({P}\right)={P}{D}{0}_{{G}}$
25 11 21 24 syl2anc ${⊢}{\phi }\to {N}\left({P}\right)={P}{D}{0}_{{G}}$
26 1 22 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {X}$
27 11 26 syl ${⊢}{\phi }\to {0}_{{G}}\in {X}$
28 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {0}_{{G}}\in {X}\right)\to {P}{D}{0}_{{G}}={0}_{{G}}{D}{P}$
29 17 21 27 28 syl3anc ${⊢}{\phi }\to {P}{D}{0}_{{G}}={0}_{{G}}{D}{P}$
30 25 29 eqtrd ${⊢}{\phi }\to {N}\left({P}\right)={0}_{{G}}{D}{P}$
31 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
32 1zzd ${⊢}{\phi }\to 1\in ℤ$
33 11 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {G}\in \mathrm{Grp}$
34 6 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\in {X}$
35 4 1 22 23 2 nmval2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {F}\left({k}\right)\in {X}\right)\to {N}\left({F}\left({k}\right)\right)={F}\left({k}\right){D}{0}_{{G}}$
36 33 34 35 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {N}\left({F}\left({k}\right)\right)={F}\left({k}\right){D}{0}_{{G}}$
37 17 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
38 27 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {0}_{{G}}\in {X}$
39 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({k}\right)\in {X}\wedge {0}_{{G}}\in {X}\right)\to {F}\left({k}\right){D}{0}_{{G}}={0}_{{G}}{D}{F}\left({k}\right)$
40 37 34 38 39 syl3anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right){D}{0}_{{G}}={0}_{{G}}{D}{F}\left({k}\right)$
41 36 40 eqtrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {N}\left({F}\left({k}\right)\right)={0}_{{G}}{D}{F}\left({k}\right)$
42 41 9 eqbrtrrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {0}_{{G}}{D}{F}\left({k}\right)\le {R}$
43 31 3 17 32 7 27 8 42 lmle ${⊢}{\phi }\to {0}_{{G}}{D}{P}\le {R}$
44 30 43 eqbrtrd ${⊢}{\phi }\to {N}\left({P}\right)\le {R}$