Theorem grplrinv

Description: In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		grplrinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grplrinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grplrinv.i	$$⊢\underset{\dot{}}{0}=0_G$$
4		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
5	1 4	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to {inv}_g\left(G\right)\left(x\right)\in B$$
6		oveq1	$$⊢y={inv}_g\left(G\right)\left(x\right)\to y\underset{\dot{}}{+}x={inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x$$
7	6	eqeq1d	$$⊢y={inv}_g\left(G\right)\left(x\right)\to \left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow {inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
8		oveq2	$$⊢y={inv}_g\left(G\right)\left(x\right)\to x\underset{\dot{}}{+}y=x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)$$
9	8	eqeq1d	$$⊢y={inv}_g\left(G\right)\left(x\right)\to \left(x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\leftrightarrow x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
10	7 9	anbi12d	$$⊢y={inv}_g\left(G\right)\left(x\right)\to \left(\left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\leftrightarrow \left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
11	10	adantl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge x\in B\right)\wedge y={inv}_g\left(G\right)\left(x\right)\right)\to \left(\left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\leftrightarrow \left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
12	1 2 3 4	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to {inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
13	1 2 3 4	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=\underset{\dot{}}{0}$$
14	12 13	jca	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
15	5 11 14	rspcedvd	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \exists y\in B\left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)$$
16	15	ralrimiva	$$⊢G\in \mathrm{Grp}\to \forall x\in B\exists y\in B\left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)$$