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 e. GrpOp /\ A e. 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 e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) )
5	4	simpld	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G A ) = U )