Theorem grplinv

Description: The left 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	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\underset{\dot{}}{+}X=\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 3 4	grpinvval	$$⊢X\in B\to N\left(X\right)=\left(\iota y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
6	5	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)=\left(\iota y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
7	1 2 3	grpinveu	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \exists !y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
8		riotacl2	$$⊢\exists !y\in By\underset{\dot{}}{+}X=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\in \left\{y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right\}$$
9	7 8	syl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(\iota y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\in \left\{y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right\}$$
10	6 9	eqeltrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in \left\{y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right\}$$
11		oveq1	$$⊢y=N\left(X\right)\to y\underset{\dot{}}{+}X=N\left(X\right)\underset{\dot{}}{+}X$$
12	11	eqeq1d	$$⊢y=N\left(X\right)\to \left(y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\leftrightarrow N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
13	12	elrab	$$⊢N\left(X\right)\in \left\{y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right\}\leftrightarrow \left(N\left(X\right)\in B\wedge N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
14	13	simprbi	$$⊢N\left(X\right)\in \left\{y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right\}\to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
15	10 14	syl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$