# 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}=\mathrm{ran}{G}$
grpoinveu.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
Assertion grpoid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left({A}={U}↔{A}{G}{A}={A}\right)$

### Proof

Step Hyp Ref Expression
1 grpoinveu.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpoinveu.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
3 1 2 grpoidcl ${⊢}{G}\in \mathrm{GrpOp}\to {U}\in {X}$
4 1 grporcan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {U}\in {X}\wedge {A}\in {X}\right)\right)\to \left({A}{G}{A}={U}{G}{A}↔{A}={U}\right)$
5 4 3exp2 ${⊢}{G}\in \mathrm{GrpOp}\to \left({A}\in {X}\to \left({U}\in {X}\to \left({A}\in {X}\to \left({A}{G}{A}={U}{G}{A}↔{A}={U}\right)\right)\right)\right)$
6 3 5 mpid ${⊢}{G}\in \mathrm{GrpOp}\to \left({A}\in {X}\to \left({A}\in {X}\to \left({A}{G}{A}={U}{G}{A}↔{A}={U}\right)\right)\right)$
7 6 pm2.43d ${⊢}{G}\in \mathrm{GrpOp}\to \left({A}\in {X}\to \left({A}{G}{A}={U}{G}{A}↔{A}={U}\right)\right)$
8 7 imp ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left({A}{G}{A}={U}{G}{A}↔{A}={U}\right)$
9 1 2 grpolid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to {U}{G}{A}={A}$
10 9 eqeq2d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left({A}{G}{A}={U}{G}{A}↔{A}{G}{A}={A}\right)$
11 8 10 bitr3d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left({A}={U}↔{A}{G}{A}={A}\right)$