This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grporinv

Description: The right 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 grporinv ( ( 𝐺 ∈ 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 simprd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 )