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