Metamath Proof Explorer


Theorem grprid

Description: The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011)

Ref Expression
Hypotheses grpbn0.b B = Base G
grplid.p + ˙ = + G
grplid.o 0 ˙ = 0 G
Assertion grprid G Grp X B X + ˙ 0 ˙ = X

Proof

Step Hyp Ref Expression
1 grpbn0.b B = Base G
2 grplid.p + ˙ = + G
3 grplid.o 0 ˙ = 0 G
4 grpmnd G Grp G Mnd
5 1 2 3 mndrid G Mnd X B X + ˙ 0 ˙ = X
6 4 5 sylan G Grp X B X + ˙ 0 ˙ = X