# 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 𝑋 = ( Base ‘ 𝐺 )
nglmle.2 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
nglmle.3 𝐽 = ( MetOpen ‘ 𝐷 )
nglmle.5 𝑁 = ( norm ‘ 𝐺 )
nglmle.6 ( 𝜑𝐺 ∈ NrmGrp )
nglmle.7 ( 𝜑𝐹 : ℕ ⟶ 𝑋 )
nglmle.8 ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑃 )
nglmle.9 ( 𝜑𝑅 ∈ ℝ* )
nglmle.10 ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑁 ‘ ( 𝐹𝑘 ) ) ≤ 𝑅 )
Assertion nglmle ( 𝜑 → ( 𝑁𝑃 ) ≤ 𝑅 )

### Proof

Step Hyp Ref Expression
1 nglmle.1 𝑋 = ( Base ‘ 𝐺 )
2 nglmle.2 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
3 nglmle.3 𝐽 = ( MetOpen ‘ 𝐷 )
4 nglmle.5 𝑁 = ( norm ‘ 𝐺 )
5 nglmle.6 ( 𝜑𝐺 ∈ NrmGrp )
6 nglmle.7 ( 𝜑𝐹 : ℕ ⟶ 𝑋 )
7 nglmle.8 ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑃 )
8 nglmle.9 ( 𝜑𝑅 ∈ ℝ* )
9 nglmle.10 ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑁 ‘ ( 𝐹𝑘 ) ) ≤ 𝑅 )
10 ngpgrp ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
11 5 10 syl ( 𝜑𝐺 ∈ Grp )
12 ngpms ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
13 5 12 syl ( 𝜑𝐺 ∈ MetSp )
14 msxms ( 𝐺 ∈ MetSp → 𝐺 ∈ ∞MetSp )
15 13 14 syl ( 𝜑𝐺 ∈ ∞MetSp )
16 1 2 xmsxmet ( 𝐺 ∈ ∞MetSp → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 15 16 syl ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 3 mopntopon ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 17 18 syl ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
20 lmcl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ) → 𝑃𝑋 )
21 19 7 20 syl2anc ( 𝜑𝑃𝑋 )
22 eqid ( 0g𝐺 ) = ( 0g𝐺 )
23 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
24 4 1 22 23 2 nmval2 ( ( 𝐺 ∈ Grp ∧ 𝑃𝑋 ) → ( 𝑁𝑃 ) = ( 𝑃 𝐷 ( 0g𝐺 ) ) )
25 11 21 24 syl2anc ( 𝜑 → ( 𝑁𝑃 ) = ( 𝑃 𝐷 ( 0g𝐺 ) ) )
26 1 22 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝑋 )
27 11 26 syl ( 𝜑 → ( 0g𝐺 ) ∈ 𝑋 )
28 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 0g𝐺 ) ∈ 𝑋 ) → ( 𝑃 𝐷 ( 0g𝐺 ) ) = ( ( 0g𝐺 ) 𝐷 𝑃 ) )
29 17 21 27 28 syl3anc ( 𝜑 → ( 𝑃 𝐷 ( 0g𝐺 ) ) = ( ( 0g𝐺 ) 𝐷 𝑃 ) )
30 25 29 eqtrd ( 𝜑 → ( 𝑁𝑃 ) = ( ( 0g𝐺 ) 𝐷 𝑃 ) )
31 nnuz ℕ = ( ℤ ‘ 1 )
32 1zzd ( 𝜑 → 1 ∈ ℤ )
33 11 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐺 ∈ Grp )
34 6 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ 𝑋 )
35 4 1 22 23 2 nmval2 ( ( 𝐺 ∈ Grp ∧ ( 𝐹𝑘 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐹𝑘 ) ) = ( ( 𝐹𝑘 ) 𝐷 ( 0g𝐺 ) ) )
36 33 34 35 syl2anc ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑁 ‘ ( 𝐹𝑘 ) ) = ( ( 𝐹𝑘 ) 𝐷 ( 0g𝐺 ) ) )
37 17 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
38 27 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( 0g𝐺 ) ∈ 𝑋 )
39 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 0g𝐺 ) ∈ 𝑋 ) → ( ( 𝐹𝑘 ) 𝐷 ( 0g𝐺 ) ) = ( ( 0g𝐺 ) 𝐷 ( 𝐹𝑘 ) ) )
40 37 34 38 39 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) 𝐷 ( 0g𝐺 ) ) = ( ( 0g𝐺 ) 𝐷 ( 𝐹𝑘 ) ) )
41 36 40 eqtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑁 ‘ ( 𝐹𝑘 ) ) = ( ( 0g𝐺 ) 𝐷 ( 𝐹𝑘 ) ) )
42 41 9 eqbrtrrd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 0g𝐺 ) 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 )
43 31 3 17 32 7 27 8 42 lmle ( 𝜑 → ( ( 0g𝐺 ) 𝐷 𝑃 ) ≤ 𝑅 )
44 30 43 eqbrtrd ( 𝜑 → ( 𝑁𝑃 ) ≤ 𝑅 )