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	⊢ 𝑋 = ran 𝐺
	grpinv.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
	grpinv.3	⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion	grpolinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		grpinv.1	⊢ 𝑋 = ran 𝐺
2		grpinv.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3		grpinv.3	⊢ 𝑁 = ( inv ‘ 𝐺 )
4	1 2 3	grpoinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) )
5	4	simpld	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 )