Metamath Proof Explorer

Theorem ngpi

Description: The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021)

Ref Expression
Hypotheses ngpi.v 
|- V = ( Base ` W )
ngpi.n 
|- N = ( norm ` W )
ngpi.m 
|- .- = ( -g ` W )
ngpi.0 
|- .0. = ( 0g ` W )
Assertion ngpi 
|- ( W e. NrmGrp -> ( W e. Grp /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ngpi.v 
 |-  V = ( Base ` W )
2 ngpi.n 
 |-  N = ( norm ` W )
3 ngpi.m 
 |-  .- = ( -g ` W )
4 ngpi.0 
 |-  .0. = ( 0g ` W )
5 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
6 1 2 nmf 
 |-  ( W e. NrmGrp -> N : V --> RR )
7 1 2 4 nmeq0 
 |-  ( ( W e. NrmGrp /\ x e. V ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
8 1 2 3 nmmtri 
 |-  ( ( W e. NrmGrp /\ x e. V /\ y e. V ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
9 8 3expa 
 |-  ( ( ( W e. NrmGrp /\ x e. V ) /\ y e. V ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
10 9 ralrimiva 
 |-  ( ( W e. NrmGrp /\ x e. V ) -> A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
11 7 10 jca 
 |-  ( ( W e. NrmGrp /\ x e. V ) -> ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
12 11 ralrimiva 
 |-  ( W e. NrmGrp -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
13 5 6 12 3jca 
 |-  ( W e. NrmGrp -> ( W e. Grp /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )