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 syl5eq 
 |-  ( ( 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 ) )