Theorem dfgrp2e

Description: Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in Lang p. 7. (Contributed by NM, 10-Oct-2006) (Revised by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp2.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	dfgrp2e	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\wedge \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfgrp2.b	$$⊢B={\mathrm{Base}}_G$$
2		dfgrp2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	dfgrp2	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(G\in \mathrm{Smgrp}\wedge \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\right)$$
4		ax-1	$$⊢G\in \mathrm{V}\to \left(n\in B\to G\in \mathrm{V}\right)$$
5		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
6	1	eleq2i	$$⊢n\in B\leftrightarrow n\in {\mathrm{Base}}_G$$
7		eleq2	$$⊢{\mathrm{Base}}_G=\varnothing \to \left(n\in {\mathrm{Base}}_G\leftrightarrow n\in \varnothing \right)$$
8		noel	$$⊢\neg n\in \varnothing$$
9	8	pm2.21i	$$⊢n\in \varnothing \to G\in \mathrm{V}$$
10	7 9	biimtrdi	$$⊢{\mathrm{Base}}_G=\varnothing \to \left(n\in {\mathrm{Base}}_G\to G\in \mathrm{V}\right)$$
11	6 10	biimtrid	$$⊢{\mathrm{Base}}_G=\varnothing \to \left(n\in B\to G\in \mathrm{V}\right)$$
12	5 11	syl	$$⊢\neg G\in \mathrm{V}\to \left(n\in B\to G\in \mathrm{V}\right)$$
13	4 12	pm2.61i	$$⊢n\in B\to G\in \mathrm{V}$$
14	13	a1d	$$⊢n\in B\to \left(\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\to G\in \mathrm{V}\right)$$
15	14	rexlimiv	$$⊢\exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\to G\in \mathrm{V}$$
16	1 2	issgrpv	$$⊢G\in \mathrm{V}\to \left(G\in \mathrm{Smgrp}\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\right)$$
17	15 16	syl	$$⊢\exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\to \left(G\in \mathrm{Smgrp}\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\right)$$
18	17	pm5.32ri	$$⊢\left(G\in \mathrm{Smgrp}\wedge \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\right)\leftrightarrow \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\wedge \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\right)$$
19	3 18	bitri	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\wedge \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\right)$$