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

Metamath Proof Explorer

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