This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isngp

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses isngp.n 
|- N = ( norm ` G )
isngp.z 
|- .- = ( -g ` G )
isngp.d 
|- D = ( dist ` G )
Assertion isngp 
|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )

Proof

Step Hyp Ref Expression
1 isngp.n 
 |-  N = ( norm ` G )
2 isngp.z 
 |-  .- = ( -g ` G )
3 isngp.d 
 |-  D = ( dist ` G )
4 elin 
 |-  ( G e. ( Grp i^i MetSp ) <-> ( G e. Grp /\ G e. MetSp ) )
5 4 anbi1i 
 |-  ( ( G e. ( Grp i^i MetSp ) /\ ( N o. .- ) C_ D ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
6 fveq2 
 |-  ( g = G -> ( norm ` g ) = ( norm ` G ) )
7 6 1 eqtr4di 
 |-  ( g = G -> ( norm ` g ) = N )
8 fveq2 
 |-  ( g = G -> ( -g ` g ) = ( -g ` G ) )
9 8 2 eqtr4di 
 |-  ( g = G -> ( -g ` g ) = .- )
10 7 9 coeq12d 
 |-  ( g = G -> ( ( norm ` g ) o. ( -g ` g ) ) = ( N o. .- ) )
11 fveq2 
 |-  ( g = G -> ( dist ` g ) = ( dist ` G ) )
12 11 3 eqtr4di 
 |-  ( g = G -> ( dist ` g ) = D )
13 10 12 sseq12d 
 |-  ( g = G -> ( ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) <-> ( N o. .- ) C_ D ) )
14 df-ngp 
 |-  NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
15 13 14 elrab2 
 |-  ( G e. NrmGrp <-> ( G e. ( Grp i^i MetSp ) /\ ( N o. .- ) C_ D ) )
16 df-3an 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
17 5 15 16 3bitr4i 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )