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	Could not format ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) with typecode |-
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	syl6bi	$$⊢{\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	Could not format ( G e. _V -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) : No typesetting found for |- ( G e. _V -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) with typecode |-
17	15 16	syl	Could not format ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) : No typesetting found for |- ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) with typecode |-
18	17	pm5.32ri	Could not format ( ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) with typecode |-
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)$$