This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )