ngpocelbl

Description: Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007) (Revised by AV, 14-Oct-2021)

	Ref	Expression
Hypotheses	ngpocelbl.n	$⊢ N = norm (G)$
	ngpocelbl.x	$⊢ X = {Base}_{G}$
	ngpocelbl.p	$⊢ \underset{˙}{+} = +_{G}$
	ngpocelbl.d	$⊢ D = {dist (G) ↾}_{(X \times X)}$
Assertion	ngpocelbl	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \underset{˙}{+} A \in (P ball (D) R) \leftrightarrow N (A) < R)$

Proof

Step	Hyp	Ref	Expression
1		ngpocelbl.n	$⊢ N = norm (G)$
2		ngpocelbl.x	$⊢ X = {Base}_{G}$
3		ngpocelbl.p	$⊢ \underset{˙}{+} = +_{G}$
4		ngpocelbl.d	$⊢ D = {dist (G) ↾}_{(X \times X)}$
5		nlmngp	$⊢ G \in NrmMod \to G \in NrmGrp$
6	2 4	ngpmet	$⊢ G \in NrmGrp \to D \in Met (X)$
7		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
8	5 6 7	3syl	$⊢ G \in NrmMod \to D \in ∞Met (X)$
9	8	anim1i	$⊢ (G \in NrmMod \land R \in ℝ^{}) \to (D \in ∞Met (X) \land R \in ℝ^{})$
10	9	3adant3	$⊢ (G \in NrmMod \land R \in ℝ^{} \land (P \in X \land A \in X)) \to (D \in ∞Met (X) \land R \in ℝ^{})$
11		simp3l	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to P \in X$
12		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
13	5 12	syl	$⊢ G \in NrmMod \to G \in Grp$
14	13	3ad2ant1	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to G \in Grp$
15		simp3	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \in X \land A \in X)$
16		3anass	$⊢ (G \in Grp \land P \in X \land A \in X) \leftrightarrow (G \in Grp \land (P \in X \land A \in X))$
17	14 15 16	sylanbrc	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (G \in Grp \land P \in X \land A \in X)$
18	2 3	grpcl	$⊢ (G \in Grp \land P \in X \land A \in X) \to P \underset{˙}{+} A \in X$
19	17 18	syl	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to P \underset{˙}{+} A \in X$
20	11 19	jca	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \in X \land P \underset{˙}{+} A \in X)$
21	10 20	jca	$⊢ (G \in NrmMod \land R \in ℝ^{} \land (P \in X \land A \in X)) \to ((D \in ∞Met (X) \land R \in ℝ^{}) \land (P \in X \land P \underset{˙}{+} A \in X))$
22		elbl2	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land P \underset{˙}{+} A \in X)) \to (P \underset{˙}{+} A \in (P ball (D) R) \leftrightarrow P D (P \underset{˙}{+} A) < R)$
23	21 22	syl	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \underset{˙}{+} A \in (P ball (D) R) \leftrightarrow P D (P \underset{˙}{+} A) < R)$
24	4	oveqi	$⊢ P D (P \underset{˙}{+} A) = P ({dist (G) ↾}_{(X \times X)}) (P \underset{˙}{+} A)$
25		ovres	$⊢ (P \in X \land P \underset{˙}{+} A \in X) \to P ({dist (G) ↾}_{(X \times X)}) (P \underset{˙}{+} A) = P dist (G) (P \underset{˙}{+} A)$
26	24 25	syl5eq	$⊢ (P \in X \land P \underset{˙}{+} A \in X) \to P D (P \underset{˙}{+} A) = P dist (G) (P \underset{˙}{+} A)$
27	20 26	syl	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to P D (P \underset{˙}{+} A) = P dist (G) (P \underset{˙}{+} A)$
28	5	3ad2ant1	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to G \in NrmGrp$
29		eqid	$⊢ -_{G} = -_{G}$
30		eqid	$⊢ dist (G) = dist (G)$
31	1 2 29 30	ngpdsr	$⊢ (G \in NrmGrp \land P \in X \land P \underset{˙}{+} A \in X) \to P dist (G) (P \underset{˙}{+} A) = N ((P \underset{˙}{+} A) -_{G} P)$
32	28 11 19 31	syl3anc	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to P dist (G) (P \underset{˙}{+} A) = N ((P \underset{˙}{+} A) -_{G} P)$
33		nlmlmod	$⊢ G \in NrmMod \to G \in LMod$
34		lmodabl	$⊢ G \in LMod \to G \in Abel$
35	33 34	syl	$⊢ G \in NrmMod \to G \in Abel$
36	35	3ad2ant1	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to G \in Abel$
37		3anass	$⊢ (G \in Abel \land P \in X \land A \in X) \leftrightarrow (G \in Abel \land (P \in X \land A \in X))$
38	36 15 37	sylanbrc	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (G \in Abel \land P \in X \land A \in X)$
39	2 3 29	ablpncan2	$⊢ (G \in Abel \land P \in X \land A \in X) \to (P \underset{˙}{+} A) -_{G} P = A$
40	38 39	syl	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \underset{˙}{+} A) -_{G} P = A$
41	40	fveq2d	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to N ((P \underset{˙}{+} A) -_{G} P) = N (A)$
42	27 32 41	3eqtrd	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to P D (P \underset{˙}{+} A) = N (A)$
43	42	breq1d	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P D (P \underset{˙}{+} A) < R \leftrightarrow N (A) < R)$
44	23 43	bitrd	$⊢ (G \in NrmMod \land R \in ℝ^{*} \land (P \in X \land A \in X)) \to (P \underset{˙}{+} A \in (P ball (D) R) \leftrightarrow N (A) < R)$

Metamath Proof Explorer

Theorem ngpocelbl

Proof