Theorem grpinvid

Description: The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinvid.u	⊢ 0 = ( 0g ‘ 𝐺 )
	grpinvid.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	grpinvid	⊢ ( 𝐺 ∈ Grp → ( 𝑁 ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		grpinvid.u	⊢ 0 = ( 0g ‘ 𝐺 )
2		grpinvid.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	3 1	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6	3 5 1	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
7	4 6	mpdan	⊢ ( 𝐺 ∈ Grp → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
8	3 5 1 2	grpinvid1	⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑁 ‘ 0 ) = 0 ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ) )
9	4 4 8	mpd3an23	⊢ ( 𝐺 ∈ Grp → ( ( 𝑁 ‘ 0 ) = 0 ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ) )
10	7 9	mpbird	⊢ ( 𝐺 ∈ Grp → ( 𝑁 ‘ 0 ) = 0 )