This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
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 ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑃 ) ≤ 𝑅 )