Theorem grporid

Description: The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpoidval.1	|- X = ran G
	grpoidval.2	|- U = ( GId ` G )
Assertion	grporid	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G U ) = A )

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	|- X = ran G
2		grpoidval.2	|- U = ( GId ` G )
3	1 2	grpoidinv2	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. x e. X ( ( x G A ) = U /\ ( A G x ) = U ) ) )
4		simplr	|- ( ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. x e. X ( ( x G A ) = U /\ ( A G x ) = U ) ) -> ( A G U ) = A )
5	3 4	syl	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G U ) = A )