Metamath Proof Explorer


Theorem 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
|- .+ = ( +g ` G )
ngpocelbl.d
|- D = ( ( dist ` G ) |` ( X X. X ) )
Assertion ngpocelbl
|- ( ( G e. NrmMod /\ R e. RR* /\ ( P e. X /\ A e. X ) ) -> ( ( P .+ A ) e. ( P ( ball ` D ) R ) <-> ( N ` A ) < R ) )

Proof

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