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