Metamath Proof Explorer


Theorem grpolinv

Description: The left inverse of a group element. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpinv.1 X = ran G
grpinv.2 U = GId G
grpinv.3 N = inv G
Assertion grpolinv G GrpOp A X N A G A = U

Proof

Step Hyp Ref Expression
1 grpinv.1 X = ran G
2 grpinv.2 U = GId G
3 grpinv.3 N = inv G
4 1 2 3 grpoinv G GrpOp A X N A G A = U A G N A = U
5 4 simpld G GrpOp A X N A G A = U