Theorem grpinvex

Description: Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinvex.p	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpinvex	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \exists y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		grpcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinvex.p	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 2 3	isgrp	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in B\exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
5	4	simprbi	$$⊢G\in \mathrm{Grp}\to \forall x\in B\exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
6		oveq2	$$⊢x=X\to y\underset{\dot{}}{+}x=y\underset{\dot{}}{+}X$$
7	6	eqeq1d	$$⊢x=X\to \left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
8	7	rexbidv	$$⊢x=X\to \left(\exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow \exists y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
9	8	rspccva	$$⊢\left(\forall x\in B\exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge X\in B\right)\to \exists y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
10	5 9	sylan	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \exists y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$