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={\mathrm{Base}}_G$$
	grplid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grplid.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$

Proof

Step	Hyp	Ref	Expression
1		grpbn0.b	$$⊢B={\mathrm{Base}}_G$$
2		grplid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grplid.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
5	1 2 3	mndrid	$$⊢\left(G\in \mathrm{Mnd}\wedge X\in B\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$
6	4 5	sylan	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$