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 )