Theorem nm0

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

	Ref	Expression
Hypotheses	nm0.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	nm0.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	nm0	$$⊢G\in \mathrm{NrmGrp}\to N\left(\underset{\dot{}}{0}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		nm0.n	$$⊢N=\mathrm{norm}\left(G\right)$$
2		nm0.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
4		ngpgrp	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{Grp}$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	5 2	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
7	4 6	syl	$$⊢G\in \mathrm{NrmGrp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
8	5 1 2	nmeq0	$$⊢\left(G\in \mathrm{NrmGrp}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \left(N\left(\underset{\dot{}}{0}\right)=0\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
9	7 8	mpdan	$$⊢G\in \mathrm{NrmGrp}\to \left(N\left(\underset{\dot{}}{0}\right)=0\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
10	3 9	mpbiri	$$⊢G\in \mathrm{NrmGrp}\to N\left(\underset{\dot{}}{0}\right)=0$$