Theorem grpoid

Description: Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		grpoinveu.1	|- X = ran G
2		grpoinveu.2	|- U = ( GId ` G )
3	1 2	grpoidcl	|- ( G e. GrpOp -> U e. X )
4	1	grporcan	|- ( ( G e. GrpOp /\ ( A e. X /\ U e. X /\ A e. X ) ) -> ( ( A G A ) = ( U G A ) <-> A = U ) )
5	4	3exp2	|- ( G e. GrpOp -> ( A e. X -> ( U e. X -> ( A e. X -> ( ( A G A ) = ( U G A ) <-> A = U ) ) ) ) )
6	3 5	mpid	|- ( G e. GrpOp -> ( A e. X -> ( A e. X -> ( ( A G A ) = ( U G A ) <-> A = U ) ) ) )
7	6	pm2.43d	|- ( G e. GrpOp -> ( A e. X -> ( ( A G A ) = ( U G A ) <-> A = U ) ) )
8	7	imp	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( A G A ) = ( U G A ) <-> A = U ) )
9	1 2	grpolid	|- ( ( G e. GrpOp /\ A e. X ) -> ( U G A ) = A )
10	9	eqeq2d	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( A G A ) = ( U G A ) <-> ( A G A ) = A ) )
11	8 10	bitr3d	|- ( ( G e. GrpOp /\ A e. X ) -> ( A = U <-> ( A G A ) = A ) )