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 ` G )
grpinvid.n 
|- N = ( invg ` G )
Assertion grpinvid 
|- ( G e. Grp -> ( N ` .0. ) = .0. )

Proof

Step Hyp Ref Expression
1 grpinvid.u 
 |-  .0. = ( 0g ` G )
2 grpinvid.n 
 |-  N = ( invg ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 1 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 3 5 1 grplid 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
7 4 6 mpdan 
 |-  ( G e. Grp -> ( .0. ( +g ` G ) .0. ) = .0. )
8 3 5 1 2 grpinvid1 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) /\ .0. e. ( Base ` G ) ) -> ( ( N ` .0. ) = .0. <-> ( .0. ( +g ` G ) .0. ) = .0. ) )
9 4 4 8 mpd3an23 
 |-  ( G e. Grp -> ( ( N ` .0. ) = .0. <-> ( .0. ( +g ` G ) .0. ) = .0. ) )
10 7 9 mpbird 
 |-  ( G e. Grp -> ( N ` .0. ) = .0. )