Metamath Proof Explorer


Theorem nm0

Description: Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nm0.n
|- N = ( norm ` G )
nm0.z
|- .0. = ( 0g ` G )
Assertion nm0
|- ( G e. NrmGrp -> ( N ` .0. ) = 0 )

Proof

Step Hyp Ref Expression
1 nm0.n
 |-  N = ( norm ` G )
2 nm0.z
 |-  .0. = ( 0g ` G )
3 eqid
 |-  .0. = .0.
4 ngpgrp
 |-  ( G e. NrmGrp -> G e. Grp )
5 eqid
 |-  ( Base ` G ) = ( Base ` G )
6 5 2 grpidcl
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
7 4 6 syl
 |-  ( G e. NrmGrp -> .0. e. ( Base ` G ) )
8 5 1 2 nmeq0
 |-  ( ( G e. NrmGrp /\ .0. e. ( Base ` G ) ) -> ( ( N ` .0. ) = 0 <-> .0. = .0. ) )
9 7 8 mpdan
 |-  ( G e. NrmGrp -> ( ( N ` .0. ) = 0 <-> .0. = .0. ) )
10 3 9 mpbiri
 |-  ( G e. NrmGrp -> ( N ` .0. ) = 0 )