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 ) |