Metamath Proof Explorer


Theorem grpolidinv

Description: A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 X=ranG
Assertion grpolidinv GGrpOpuXxXuGx=xyXyGx=u

Proof

Step Hyp Ref Expression
1 grpfo.1 X=ranG
2 1 isgrpo GGrpOpGGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
3 2 ibi GGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
4 3 simp3d GGrpOpuXxXuGx=xyXyGx=u