Metamath Proof Explorer

Theorem nmsub

Description: The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nmmtri.m 
|- .- = ( -g ` G )
Assertion nmsub 
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) = ( N ` ( B .- A ) ) )

Proof

Step Hyp Ref Expression
1 nmf.x 
 |-  X = ( Base ` G )
2 nmf.n 
 |-  N = ( norm ` G )
3 nmmtri.m 
 |-  .- = ( -g ` G )
4 simp1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. NrmGrp )
5 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
6 4 5 syl 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. Grp )
7 simp3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> B e. X )
8 simp2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> A e. X )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 1 3 9 grpinvsub 
 |-  ( ( G e. Grp /\ B e. X /\ A e. X ) -> ( ( invg ` G ) ` ( B .- A ) ) = ( A .- B ) )
11 6 7 8 10 syl3anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( invg ` G ) ` ( B .- A ) ) = ( A .- B ) )
12 11 fveq2d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( ( invg ` G ) ` ( B .- A ) ) ) = ( N ` ( A .- B ) ) )
13 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ B e. X /\ A e. X ) -> ( B .- A ) e. X )
14 6 7 8 13 syl3anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( B .- A ) e. X )
15 1 2 9 nminv 
 |-  ( ( G e. NrmGrp /\ ( B .- A ) e. X ) -> ( N ` ( ( invg ` G ) ` ( B .- A ) ) ) = ( N ` ( B .- A ) ) )
16 4 14 15 syl2anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( ( invg ` G ) ` ( B .- A ) ) ) = ( N ` ( B .- A ) ) )
17 12 16 eqtr3d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) = ( N ` ( B .- A ) ) )