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=normG
ngpocelbl.x X=BaseG
ngpocelbl.p +˙=+G
ngpocelbl.d D=distGX×X
Assertion ngpocelbl GNrmModR*PXAXP+˙APballDRNA<R

Proof

Step Hyp Ref Expression
1 ngpocelbl.n N=normG
2 ngpocelbl.x X=BaseG
3 ngpocelbl.p +˙=+G
4 ngpocelbl.d D=distGX×X
5 nlmngp GNrmModGNrmGrp
6 2 4 ngpmet GNrmGrpDMetX
7 metxmet DMetXD∞MetX
8 5 6 7 3syl GNrmModD∞MetX
9 8 anim1i GNrmModR*D∞MetXR*
10 9 3adant3 GNrmModR*PXAXD∞MetXR*
11 simp3l GNrmModR*PXAXPX
12 ngpgrp GNrmGrpGGrp
13 5 12 syl GNrmModGGrp
14 13 3ad2ant1 GNrmModR*PXAXGGrp
15 simp3 GNrmModR*PXAXPXAX
16 3anass GGrpPXAXGGrpPXAX
17 14 15 16 sylanbrc GNrmModR*PXAXGGrpPXAX
18 2 3 grpcl GGrpPXAXP+˙AX
19 17 18 syl GNrmModR*PXAXP+˙AX
20 11 19 jca GNrmModR*PXAXPXP+˙AX
21 10 20 jca GNrmModR*PXAXD∞MetXR*PXP+˙AX
22 elbl2 D∞MetXR*PXP+˙AXP+˙APballDRPDP+˙A<R
23 21 22 syl GNrmModR*PXAXP+˙APballDRPDP+˙A<R
24 4 oveqi PDP+˙A=PdistGX×XP+˙A
25 ovres PXP+˙AXPdistGX×XP+˙A=PdistGP+˙A
26 24 25 eqtrid PXP+˙AXPDP+˙A=PdistGP+˙A
27 20 26 syl GNrmModR*PXAXPDP+˙A=PdistGP+˙A
28 5 3ad2ant1 GNrmModR*PXAXGNrmGrp
29 eqid -G=-G
30 eqid distG=distG
31 1 2 29 30 ngpdsr GNrmGrpPXP+˙AXPdistGP+˙A=NP+˙A-GP
32 28 11 19 31 syl3anc GNrmModR*PXAXPdistGP+˙A=NP+˙A-GP
33 nlmlmod GNrmModGLMod
34 lmodabl GLModGAbel
35 33 34 syl GNrmModGAbel
36 35 3ad2ant1 GNrmModR*PXAXGAbel
37 3anass GAbelPXAXGAbelPXAX
38 36 15 37 sylanbrc GNrmModR*PXAXGAbelPXAX
39 2 3 29 ablpncan2 GAbelPXAXP+˙A-GP=A
40 38 39 syl GNrmModR*PXAXP+˙A-GP=A
41 40 fveq2d GNrmModR*PXAXNP+˙A-GP=NA
42 27 32 41 3eqtrd GNrmModR*PXAXPDP+˙A=NA
43 42 breq1d GNrmModR*PXAXPDP+˙A<RNA<R
44 23 43 bitrd GNrmModR*PXAXP+˙APballDRNA<R