Theorem grpinveu

Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of Herstein p. 55. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinveu.b	$$⊢B={\mathrm{Base}}_G$$
	grpinveu.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinveu.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpinveu	$$⊢\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		grpinveu.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinveu.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinveu.o	$$⊢\underset{\dot{}}{0}=0_G$$
4	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}$$
5		eqtr3	$$⊢\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y\underset{\dot{}}{+}X=z\underset{\dot{}}{+}X$$
6	1 2	grprcan	$$⊢\left(G\in \mathrm{Grp}\wedge \left(y\in B\wedge z\in B\wedge X\in B\right)\right)\to \left(y\underset{\dot{}}{+}X=z\underset{\dot{}}{+}X\leftrightarrow y=z\right)$$
7	5 6	imbitrid	$$⊢\left(G\in \mathrm{Grp}\wedge \left(y\in B\wedge z\in B\wedge X\in B\right)\right)\to \left(\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y=z\right)$$
8	7	3exp2	$$⊢G\in \mathrm{Grp}\to \left(y\in B\to \left(z\in B\to \left(X\in B\to \left(\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y=z\right)\right)\right)\right)$$
9	8	com24	$$⊢G\in \mathrm{Grp}\to \left(X\in B\to \left(z\in B\to \left(y\in B\to \left(\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y=z\right)\right)\right)\right)$$
10	9	imp41	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge X\in B\right)\wedge z\in B\right)\wedge y\in B\right)\to \left(\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y=z\right)$$
11	10	an32s	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge X\in B\right)\wedge y\in B\right)\wedge z\in B\right)\to \left(\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to y=z\right)$$
12	11	expd	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge X\in B\right)\wedge y\in B\right)\wedge z\in B\right)\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to \left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)$$
13	12	ralrimdva	$$⊢\left(\left(G\in \mathrm{Grp}\wedge X\in B\right)\wedge y\in B\right)\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to \forall z\in B\left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)$$
14	13	ancld	$$⊢\left(\left(G\in \mathrm{Grp}\wedge X\in B\right)\wedge y\in B\right)\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge \forall z\in B\left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)\right)$$
15	14	reximdva	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(\exists y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to \exists y\in B\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge \forall z\in B\left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)\right)$$
16	4 15	mpd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \exists y\in B\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge \forall z\in B\left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)$$
17		oveq1	$$⊢y=z\to y\underset{\dot{}}{+}X=z\underset{\dot{}}{+}X$$
18	17	eqeq1d	$$⊢y=z\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\leftrightarrow z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
19	18	reu8	$$⊢\exists !y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}\leftrightarrow \exists y\in B\left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\wedge \forall z\in B\left(z\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to y=z\right)\right)$$
20	16 19	sylibr	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \exists !y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$