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

Metamath Proof Explorer

Theorem grporid

Description: The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpoidval.1 ⊢ 𝑋 = ran 𝐺
grpoidval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion grporid ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑈 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 grpoidval.1 ⊢ 𝑋 = ran 𝐺
2 grpoidval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 1 2 grpoidinv2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑥 ) = 𝑈 ) ) )
4 simplr ⊢ ( ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑥 ) = 𝑈 ) ) → ( 𝐴 𝐺 𝑈 ) = 𝐴 )
5 3 4 syl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑈 ) = 𝐴 )