Theorem grpidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised 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	grpidinv2	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A=A\wedge A\underset{\dot{}}{+}\underset{\dot{}}{0}=A\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\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	1 2 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}A=A$$
5	1 2 3	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to A\underset{\dot{}}{+}\underset{\dot{}}{0}=A$$
6	1 2 3	grplrinv	$$⊢G\in \mathrm{Grp}\to \forall z\in B\exists y\in B\left(y\underset{\dot{}}{+}z=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)$$
7		oveq2	$$⊢z=A\to y\underset{\dot{}}{+}z=y\underset{\dot{}}{+}A$$
8	7	eqeq1d	$$⊢z=A\to \left(y\underset{\dot{}}{+}z=\underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\right)$$
9		oveq1	$$⊢z=A\to z\underset{\dot{}}{+}y=A\underset{\dot{}}{+}y$$
10	9	eqeq1d	$$⊢z=A\to \left(z\underset{\dot{}}{+}y=\underset{\dot{}}{0}\leftrightarrow A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)$$
11	8 10	anbi12d	$$⊢z=A\to \left(\left(y\underset{\dot{}}{+}z=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\leftrightarrow \left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\right)$$
12	11	rexbidv	$$⊢z=A\to \left(\exists y\in B\left(y\underset{\dot{}}{+}z=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\leftrightarrow \exists y\in B\left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\right)$$
13	12	rspcv	$$⊢A\in B\to \left(\forall z\in B\exists y\in B\left(y\underset{\dot{}}{+}z=\underset{\dot{}}{0}\wedge z\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\to \exists y\in B\left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\right)$$
14	6 13	mpan9	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to \exists y\in B\left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)$$
15	4 5 14	jca31	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A=A\wedge A\underset{\dot{}}{+}\underset{\dot{}}{0}=A\right)\wedge \exists y\in B\left(y\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}y=\underset{\dot{}}{0}\right)\right)$$