Metamath Proof Explorer

Theorem isngp4

Description: Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015)

Ref Expression
Hypotheses ngprcan.x 
|- X = ( Base ` G )
ngprcan.p 
|- .+ = ( +g ` G )
ngprcan.d 
|- D = ( dist ` G )
Assertion isngp4 
|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) )

Proof

Step Hyp Ref Expression
1 ngprcan.x 
 |-  X = ( Base ` G )
2 ngprcan.p 
 |-  .+ = ( +g ` G )
3 ngprcan.d 
 |-  D = ( dist ` G )
4 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
5 ngpms 
 |-  ( G e. NrmGrp -> G e. MetSp )
6 1 2 3 ngprcan 
 |-  ( ( G e. NrmGrp /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) )
7 6 ralrimivvva 
 |-  ( G e. NrmGrp -> A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) )
8 4 5 7 3jca 
 |-  ( G e. NrmGrp -> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) )
9 simp1 
 |-  ( ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) -> G e. Grp )
10 simp2 
 |-  ( ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) -> G e. MetSp )
11 eqid 
 |-  ( invg ` G ) = ( invg ` G )
12 1 11 grpinvcl 
 |-  ( ( G e. Grp /\ y e. X ) -> ( ( invg ` G ) ` y ) e. X )
13 12 ad2ant2rl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( invg ` G ) ` y ) e. X )
14 eqcom 
 |-  ( ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) <-> ( x D y ) = ( ( x .+ z ) D ( y .+ z ) ) )
15 oveq2 
 |-  ( z = ( ( invg ` G ) ` y ) -> ( x .+ z ) = ( x .+ ( ( invg ` G ) ` y ) ) )
16 oveq2 
 |-  ( z = ( ( invg ` G ) ` y ) -> ( y .+ z ) = ( y .+ ( ( invg ` G ) ` y ) ) )
17 15 16 oveq12d 
 |-  ( z = ( ( invg ` G ) ` y ) -> ( ( x .+ z ) D ( y .+ z ) ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) )
18 17 eqeq2d 
 |-  ( z = ( ( invg ` G ) ` y ) -> ( ( x D y ) = ( ( x .+ z ) D ( y .+ z ) ) <-> ( x D y ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) ) )
19 14 18 bitrid 
 |-  ( z = ( ( invg ` G ) ` y ) -> ( ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) <-> ( x D y ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) ) )
20 19 rspcv 
 |-  ( ( ( invg ` G ) ` y ) e. X -> ( A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) -> ( x D y ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) ) )
21 13 20 syl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) -> ( x D y ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) ) )
22 eqid 
 |-  ( -g ` G ) = ( -g ` G )
23 1 2 11 22 grpsubval 
 |-  ( ( x e. X /\ y e. X ) -> ( x ( -g ` G ) y ) = ( x .+ ( ( invg ` G ) ` y ) ) )
24 23 adantl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( x ( -g ` G ) y ) = ( x .+ ( ( invg ` G ) ` y ) ) )
25 24 eqcomd 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( x .+ ( ( invg ` G ) ` y ) ) = ( x ( -g ` G ) y ) )
26 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
27 1 2 26 11 grprinv 
 |-  ( ( G e. Grp /\ y e. X ) -> ( y .+ ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
28 27 ad2ant2rl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( y .+ ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
29 25 28 oveq12d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) = ( ( x ( -g ` G ) y ) D ( 0g ` G ) ) )
30 1 22 grpsubcl 
 |-  ( ( G e. Grp /\ x e. X /\ y e. X ) -> ( x ( -g ` G ) y ) e. X )
31 30 3expb 
 |-  ( ( G e. Grp /\ ( x e. X /\ y e. X ) ) -> ( x ( -g ` G ) y ) e. X )
32 31 adantlr 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( x ( -g ` G ) y ) e. X )
33 eqid 
 |-  ( norm ` G ) = ( norm ` G )
34 33 1 26 3 nmval 
 |-  ( ( x ( -g ` G ) y ) e. X -> ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) = ( ( x ( -g ` G ) y ) D ( 0g ` G ) ) )
35 32 34 syl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) = ( ( x ( -g ` G ) y ) D ( 0g ` G ) ) )
36 29 35 eqtr4d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) )
37 36 eqeq2d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = ( ( x .+ ( ( invg ` G ) ` y ) ) D ( y .+ ( ( invg ` G ) ` y ) ) ) <-> ( x D y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) ) )
38 21 37 sylibd 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) -> ( x D y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) ) )
39 38 ralimdvva 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) -> A. x e. X A. y e. X ( x D y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) ) )
40 39 3impia 
 |-  ( ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) -> A. x e. X A. y e. X ( x D y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) )
41 33 22 3 1 isngp3 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) ) )
42 9 10 40 41 syl3anbrc 
 |-  ( ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) -> G e. NrmGrp )
43 8 42 impbii 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) )