Step |
Hyp |
Ref |
Expression |
1 |
|
ngpds2.x |
|- X = ( Base ` G ) |
2 |
|
ngpds2.z |
|- .0. = ( 0g ` G ) |
3 |
|
ngpds2.m |
|- .- = ( -g ` G ) |
4 |
|
ngpds2.d |
|- D = ( dist ` G ) |
5 |
|
eqid |
|- ( norm ` G ) = ( norm ` G ) |
6 |
5 1 3 4
|
ngpds |
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( norm ` G ) ` ( A .- B ) ) ) |
7 |
|
ngpgrp |
|- ( G e. NrmGrp -> G e. Grp ) |
8 |
1 3
|
grpsubcl |
|- ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X ) |
9 |
7 8
|
syl3an1 |
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X ) |
10 |
5 1 2 4
|
nmval |
|- ( ( A .- B ) e. X -> ( ( norm ` G ) ` ( A .- B ) ) = ( ( A .- B ) D .0. ) ) |
11 |
9 10
|
syl |
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( norm ` G ) ` ( A .- B ) ) = ( ( A .- B ) D .0. ) ) |
12 |
6 11
|
eqtrd |
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( A .- B ) D .0. ) ) |