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=\mathrm{ran}G$$
	grpinv.2	$$⊢U=\mathrm{GId}\left(G\right)$$
	grpinv.3	$$⊢N=\mathrm{inv}\left(G\right)$$
Assertion	grpolinv	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to N\left(A\right)GA=U$$

Proof

Step	Hyp	Ref	Expression
1		grpinv.1	$$⊢X=\mathrm{ran}G$$
2		grpinv.2	$$⊢U=\mathrm{GId}\left(G\right)$$
3		grpinv.3	$$⊢N=\mathrm{inv}\left(G\right)$$
4	1 2 3	grpoinv	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to \left(N\left(A\right)GA=U\wedge AGN\left(A\right)=U\right)$$
5	4	simpld	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to N\left(A\right)GA=U$$