Step |
Hyp |
Ref |
Expression |
1 |
|
nmf.x |
|- X = ( Base ` G ) |
2 |
|
nmf.n |
|- N = ( norm ` G ) |
3 |
|
nminv.i |
|- I = ( invg ` G ) |
4 |
|
ngpgrp |
|- ( G e. NrmGrp -> G e. Grp ) |
5 |
4
|
adantr |
|- ( ( G e. NrmGrp /\ A e. X ) -> G e. Grp ) |
6 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
7 |
1 6
|
grpidcl |
|- ( G e. Grp -> ( 0g ` G ) e. X ) |
8 |
5 7
|
syl |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( 0g ` G ) e. X ) |
9 |
|
eqid |
|- ( -g ` G ) = ( -g ` G ) |
10 |
|
eqid |
|- ( dist ` G ) = ( dist ` G ) |
11 |
2 1 9 10
|
ngpdsr |
|- ( ( G e. NrmGrp /\ A e. X /\ ( 0g ` G ) e. X ) -> ( A ( dist ` G ) ( 0g ` G ) ) = ( N ` ( ( 0g ` G ) ( -g ` G ) A ) ) ) |
12 |
8 11
|
mpd3an3 |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( A ( dist ` G ) ( 0g ` G ) ) = ( N ` ( ( 0g ` G ) ( -g ` G ) A ) ) ) |
13 |
2 1 6 10
|
nmval |
|- ( A e. X -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) ) |
14 |
13
|
adantl |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) ) |
15 |
1 9 3 6
|
grpinvval2 |
|- ( ( G e. Grp /\ A e. X ) -> ( I ` A ) = ( ( 0g ` G ) ( -g ` G ) A ) ) |
16 |
4 15
|
sylan |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( I ` A ) = ( ( 0g ` G ) ( -g ` G ) A ) ) |
17 |
16
|
fveq2d |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` ( I ` A ) ) = ( N ` ( ( 0g ` G ) ( -g ` G ) A ) ) ) |
18 |
12 14 17
|
3eqtr4rd |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` ( I ` A ) ) = ( N ` A ) ) |