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 | |
|
ngpocelbl.x | |
||
ngpocelbl.p | |
||
ngpocelbl.d | |
||
Assertion | ngpocelbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ngpocelbl.n | |
|
2 | ngpocelbl.x | |
|
3 | ngpocelbl.p | |
|
4 | ngpocelbl.d | |
|
5 | nlmngp | |
|
6 | 2 4 | ngpmet | |
7 | metxmet | |
|
8 | 5 6 7 | 3syl | |
9 | 8 | anim1i | |
10 | 9 | 3adant3 | |
11 | simp3l | |
|
12 | ngpgrp | |
|
13 | 5 12 | syl | |
14 | 13 | 3ad2ant1 | |
15 | simp3 | |
|
16 | 3anass | |
|
17 | 14 15 16 | sylanbrc | |
18 | 2 3 | grpcl | |
19 | 17 18 | syl | |
20 | 11 19 | jca | |
21 | 10 20 | jca | |
22 | elbl2 | |
|
23 | 21 22 | syl | |
24 | 4 | oveqi | |
25 | ovres | |
|
26 | 24 25 | eqtrid | |
27 | 20 26 | syl | |
28 | 5 | 3ad2ant1 | |
29 | eqid | |
|
30 | eqid | |
|
31 | 1 2 29 30 | ngpdsr | |
32 | 28 11 19 31 | syl3anc | |
33 | nlmlmod | |
|
34 | lmodabl | |
|
35 | 33 34 | syl | |
36 | 35 | 3ad2ant1 | |
37 | 3anass | |
|
38 | 36 15 37 | sylanbrc | |
39 | 2 3 29 | ablpncan2 | |
40 | 38 39 | syl | |
41 | 40 | fveq2d | |
42 | 27 32 41 | 3eqtrd | |
43 | 42 | breq1d | |
44 | 23 43 | bitrd | |