Metamath Proof Explorer

Theorem nminv

Description: The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nminv.i 
|- I = ( invg ` G )
Assertion nminv 
|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` ( I ` A ) ) = ( N ` A ) )

Proof

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