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	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑃 ) ≤ 𝑅 )