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 )