Theorem grprinv

Description: The right inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpinv.b	$$⊢B={\mathrm{Base}}_G$$
	grpinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinv.u	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinv.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{+}N\left(X\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		grpinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinv.u	$$⊢\underset{\dot{}}{0}=0_G$$
4		grpinv.n	$$⊢N={inv}_g\left(G\right)$$
5	1 2	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
6	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
7	1 2 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
8	1 2	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
9	1 2 3	grpinvex	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
10		simpr	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\in B$$
11	1 4	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
12	1 2 3 4	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
13	5 6 7 8 9 10 11 12	grprinvd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{+}N\left(X\right)=\underset{\dot{}}{0}$$