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=ranG
grpoinveu.2 U=GIdG
Assertion grpoid GGrpOpAXA=UAGA=A

Proof

Step Hyp Ref Expression
1 grpoinveu.1 X=ranG
2 grpoinveu.2 U=GIdG
3 1 2 grpoidcl GGrpOpUX
4 1 grporcan GGrpOpAXUXAXAGA=UGAA=U
5 4 3exp2 GGrpOpAXUXAXAGA=UGAA=U
6 3 5 mpid GGrpOpAXAXAGA=UGAA=U
7 6 pm2.43d GGrpOpAXAGA=UGAA=U
8 7 imp GGrpOpAXAGA=UGAA=U
9 1 2 grpolid GGrpOpAXUGA=A
10 9 eqeq2d GGrpOpAXAGA=UGAAGA=A
11 8 10 bitr3d GGrpOpAXA=UAGA=A