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 𝑋 = 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 ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) 𝐺 𝐴 ) = 𝑈 )