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

Metamath Proof Explorer

Theorem nmf2

Description: The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmf2.n 
|- N = ( norm ` W )
nmf2.x 
|- X = ( Base ` W )
nmf2.d 
|- D = ( dist ` W )
nmf2.e 
|- E = ( D |` ( X X. X ) )
Assertion nmf2 
|- ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )

Proof

Step Hyp Ref Expression
1 nmf2.n 
 |-  N = ( norm ` W )
2 nmf2.x 
 |-  X = ( Base ` W )
3 nmf2.d 
 |-  D = ( dist ` W )
4 nmf2.e 
 |-  E = ( D |` ( X X. X ) )
5 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
6 1 2 5 3 4 nmfval2 
 |-  ( W e. Grp -> N = ( x e. X |-> ( x E ( 0g ` W ) ) ) )
7 6 adantr 
 |-  ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N = ( x e. X |-> ( x E ( 0g ` W ) ) ) )
8 2 5 grpidcl 
 |-  ( W e. Grp -> ( 0g ` W ) e. X )
9 metcl 
 |-  ( ( E e. ( Met ` X ) /\ x e. X /\ ( 0g ` W ) e. X ) -> ( x E ( 0g ` W ) ) e. RR )
10 9 3comr 
 |-  ( ( ( 0g ` W ) e. X /\ E e. ( Met ` X ) /\ x e. X ) -> ( x E ( 0g ` W ) ) e. RR )
11 8 10 syl3an1 
 |-  ( ( W e. Grp /\ E e. ( Met ` X ) /\ x e. X ) -> ( x E ( 0g ` W ) ) e. RR )
12 11 3expa 
 |-  ( ( ( W e. Grp /\ E e. ( Met ` X ) ) /\ x e. X ) -> ( x E ( 0g ` W ) ) e. RR )
13 7 12 fmpt3d 
 |-  ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )