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