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. )