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	⊢ 𝑁 = ( norm ‘ 𝐺 )
	ngpocelbl.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ngpocelbl.p	⊢ + = ( +_g ‘ 𝐺 )
	ngpocelbl.d	⊢ 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	ngpocelbl	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑃 + 𝐴 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑁 ‘ 𝐴 ) < 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ngpocelbl.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
2		ngpocelbl.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
3		ngpocelbl.p	⊢ + = ( +_g ‘ 𝐺 )
4		ngpocelbl.d	⊢ 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
5		nlmngp	⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ NrmGrp )
6	2 4	ngpmet	⊢ ( 𝐺 ∈ NrmGrp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
7		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8	5 6 7	3syl	⊢ ( 𝐺 ∈ NrmMod → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9	8	anim1i	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) )
10	9	3adant3	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) )
11		simp3l	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝑃 ∈ 𝑋 )
12		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
13	5 12	syl	⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ Grp )
14	13	3ad2ant1	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
15		simp3	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
16		3anass	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
17	14 15 16	sylanbrc	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
18	2 3	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 + 𝐴 ) ∈ 𝑋 )
19	17 18	syl	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 + 𝐴 ) ∈ 𝑋 )
20	11 19	jca	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) )
21	10 20	jca	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) ) )
22		elbl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) ) → ( ( 𝑃 + 𝐴 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) < 𝑅 ) )
23	21 22	syl	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑃 + 𝐴 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) < 𝑅 ) )
24	4	oveqi	⊢ ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) = ( 𝑃 ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) ( 𝑃 + 𝐴 ) )
25		ovres	⊢ ( ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) → ( 𝑃 ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) ( 𝑃 + 𝐴 ) ) = ( 𝑃 ( dist ‘ 𝐺 ) ( 𝑃 + 𝐴 ) ) )
26	24 25	syl5eq	⊢ ( ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) → ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) = ( 𝑃 ( dist ‘ 𝐺 ) ( 𝑃 + 𝐴 ) ) )
27	20 26	syl	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) = ( 𝑃 ( dist ‘ 𝐺 ) ( 𝑃 + 𝐴 ) ) )
28	5	3ad2ant1	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐺 ∈ NrmGrp )
29		eqid	⊢ ( -_g ‘ 𝐺 ) = ( -_g ‘ 𝐺 )
30		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
31	1 2 29 30	ngpdsr	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑃 + 𝐴 ) ∈ 𝑋 ) → ( 𝑃 ( dist ‘ 𝐺 ) ( 𝑃 + 𝐴 ) ) = ( 𝑁 ‘ ( ( 𝑃 + 𝐴 ) ( -_g ‘ 𝐺 ) 𝑃 ) ) )
32	28 11 19 31	syl3anc	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 ( dist ‘ 𝐺 ) ( 𝑃 + 𝐴 ) ) = ( 𝑁 ‘ ( ( 𝑃 + 𝐴 ) ( -_g ‘ 𝐺 ) 𝑃 ) ) )
33		nlmlmod	⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ LMod )
34		lmodabl	⊢ ( 𝐺 ∈ LMod → 𝐺 ∈ Abel )
35	33 34	syl	⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ Abel )
36	35	3ad2ant1	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐺 ∈ Abel )
37		3anass	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ↔ ( 𝐺 ∈ Abel ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
38	36 15 37	sylanbrc	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
39	2 3 29	ablpncan2	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 + 𝐴 ) ( -_g ‘ 𝐺 ) 𝑃 ) = 𝐴 )
40	38 39	syl	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑃 + 𝐴 ) ( -_g ‘ 𝐺 ) 𝑃 ) = 𝐴 )
41	40	fveq2d	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( ( 𝑃 + 𝐴 ) ( -_g ‘ 𝐺 ) 𝑃 ) ) = ( 𝑁 ‘ 𝐴 ) )
42	27 32 41	3eqtrd	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
43	42	breq1d	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑃 𝐷 ( 𝑃 + 𝐴 ) ) < 𝑅 ↔ ( 𝑁 ‘ 𝐴 ) < 𝑅 ) )
44	23 43	bitrd	⊢ ( ( 𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑃 + 𝐴 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑁 ‘ 𝐴 ) < 𝑅 ) )

Metamath Proof Explorer

Theorem ngpocelbl

Proof