Theorem grpidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (Revised by AV, 1-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		grpidinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpidinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		eqid	$$⊢0_G=0_G$$
4	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
5		oveq1	$$⊢u=0_G\to u\underset{\dot{}}{+}x=0_G\underset{\dot{}}{+}x$$
6	5	eqeq1d	$$⊢u=0_G\to \left(u\underset{\dot{}}{+}x=x\leftrightarrow 0_G\underset{\dot{}}{+}x=x\right)$$
7		oveq2	$$⊢u=0_G\to x\underset{\dot{}}{+}u=x\underset{\dot{}}{+}{0}_G$$
8	7	eqeq1d	$$⊢u=0_G\to \left(x\underset{\dot{}}{+}u=x\leftrightarrow x\underset{\dot{}}{+}{0}_G=x\right)$$
9	6 8	anbi12d	$$⊢u=0_G\to \left(\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\leftrightarrow \left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\right)$$
10		eqeq2	$$⊢u=0_G\to \left(y\underset{\dot{}}{+}x=u\leftrightarrow y\underset{\dot{}}{+}x=0_G\right)$$
11		eqeq2	$$⊢u=0_G\to \left(x\underset{\dot{}}{+}y=u\leftrightarrow x\underset{\dot{}}{+}y=0_G\right)$$
12	10 11	anbi12d	$$⊢u=0_G\to \left(\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\leftrightarrow \left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)$$
13	12	rexbidv	$$⊢u=0_G\to \left(\exists y\in B\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\leftrightarrow \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)$$
14	9 13	anbi12d	$$⊢u=0_G\to \left(\left(\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\right)\leftrightarrow \left(\left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)\right)$$
15	14	ralbidv	$$⊢u=0_G\to \left(\forall x\in B\left(\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\right)\leftrightarrow \forall x\in B\left(\left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)\right)$$
16	15	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge u=0_G\right)\to \left(\forall x\in B\left(\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\right)\leftrightarrow \forall x\in B\left(\left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)\right)$$
17	1 2 3	grpidinv2	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \left(\left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)$$
18	17	ralrimiva	$$⊢G\in \mathrm{Grp}\to \forall x\in B\left(\left(0_G\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}{0}_G=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=0_G\wedge x\underset{\dot{}}{+}y=0_G\right)\right)$$
19	4 16 18	rspcedvd	$$⊢G\in \mathrm{Grp}\to \exists u\in B\forall x\in B\left(\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}x=u\wedge x\underset{\dot{}}{+}y=u\right)\right)$$