Theorem nm0

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

	Ref	Expression
Hypotheses	nm0.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	nm0.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	nm0	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		nm0.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
2		nm0.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		eqid	⊢ 0 = 0
4		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	5 2	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
7	4 6	syl	⊢ ( 𝐺 ∈ NrmGrp → 0 ∈ ( Base ‘ 𝐺 ) )
8	5 1 2	nmeq0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑁 ‘ 0 ) = 0 ↔ 0 = 0 ) )
9	7 8	mpdan	⊢ ( 𝐺 ∈ NrmGrp → ( ( 𝑁 ‘ 0 ) = 0 ↔ 0 = 0 ) )
10	3 9	mpbiri	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 ‘ 0 ) = 0 )