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 \times X)}$
	nglmle.3	$⊢ J = MetOpen (D)$
	nglmle.5	$⊢ N = norm (G)$
	nglmle.6	$⊢ φ \to G \in NrmGrp$
	nglmle.7	$⊢ φ \to F : ℕ ⟶ X$
	nglmle.8	$⊢ φ \to F \underset{t}{⇝} (J) P$
	nglmle.9	$⊢ φ \to R \in ℝ^{*}$
	nglmle.10	$⊢ (φ \land k \in ℕ) \to N (F (k)) \leq R$
Assertion	nglmle	$⊢ φ \to N (P) \leq R$

Proof

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

Metamath Proof Explorer

Theorem nglmle

Proof