Theorem dfgrp2

Description: Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp , based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp2.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	dfgrp2	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		dfgrp2.b	$$⊢B={\mathrm{Base}}_G$$
2		dfgrp2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsgrp	Could not format ( G e. Grp -> G e. Smgrp ) : No typesetting found for |- ( G e. Grp -> G e. Smgrp ) with typecode |-
4		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
5		eqid	$$⊢0_G=0_G$$
6	1 5	mndidcl	$$⊢G\in \mathrm{Mnd}\to 0_G\in B$$
7	4 6	syl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
8		oveq1	$$⊢n=0_G\to n\underset{\dot{}}{+}x=0_G\underset{\dot{}}{+}x$$
9	8	eqeq1d	$$⊢n=0_G\to \left(n\underset{\dot{}}{+}x=x\leftrightarrow 0_G\underset{\dot{}}{+}x=x\right)$$
10		eqeq2	$$⊢n=0_G\to \left(i\underset{\dot{}}{+}x=n\leftrightarrow i\underset{\dot{}}{+}x=0_G\right)$$
11	10	rexbidv	$$⊢n=0_G\to \left(\exists i\in Bi\underset{\dot{}}{+}x=n\leftrightarrow \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)$$
12	9 11	anbi12d	$$⊢n=0_G\to \left(\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\leftrightarrow \left(0_G\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)\right)$$
13	12	ralbidv	$$⊢n=0_G\to \left(\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\leftrightarrow \forall x\in B\left(0_G\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)\right)$$
14	13	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge n=0_G\right)\to \left(\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\leftrightarrow \forall x\in B\left(0_G\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)\right)$$
15	1 2 5	mndlid	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to 0_G\underset{\dot{}}{+}x=x$$
16	4 15	sylan	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to 0_G\underset{\dot{}}{+}x=x$$
17	1 2 5	grpinvex	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \exists i\in Bi\underset{\dot{}}{+}x=0_G$$
18	16 17	jca	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \left(0_G\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)$$
19	18	ralrimiva	$$⊢G\in \mathrm{Grp}\to \forall x\in B\left(0_G\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=0_G\right)$$
20	7 14 19	rspcedvd	$$⊢G\in \mathrm{Grp}\to \exists n\in B\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)$$
21	3 20	jca	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 |-
22	1	a1i	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> B = ( Base ` G ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> B = ( Base ` G ) ) with typecode |-
23	2	a1i	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> .+ = ( +g ` G ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> .+ = ( +g ` G ) ) with typecode |-
24		sgrpmgm	Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
25	24	adantl	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Mgm ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Mgm ) with typecode |-
26	1 2	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge a\in B\wedge b\in B\right)\to a\underset{\dot{}}{+}b\in B$$
27	25 26	syl3an1	Could not format ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B /\ b e. B ) -> ( a .+ b ) e. B ) : No typesetting found for |- ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B /\ b e. B ) -> ( a .+ b ) e. B ) with typecode |-
28	1 2	sgrpass	Could not format ( ( G e. Smgrp /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) with typecode |-
29	28	adantll	Could not format ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) : No typesetting found for |- ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) with typecode |-
30		simpll	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> n e. B ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> n e. B ) with typecode |-
31		oveq2	$$⊢x=a\to n\underset{\dot{}}{+}x=n\underset{\dot{}}{+}a$$
32		id	$$⊢x=a\to x=a$$
33	31 32	eqeq12d	$$⊢x=a\to \left(n\underset{\dot{}}{+}x=x\leftrightarrow n\underset{\dot{}}{+}a=a\right)$$
34		oveq2	$$⊢x=a\to i\underset{\dot{}}{+}x=i\underset{\dot{}}{+}a$$
35	34	eqeq1d	$$⊢x=a\to \left(i\underset{\dot{}}{+}x=n\leftrightarrow i\underset{\dot{}}{+}a=n\right)$$
36	35	rexbidv	$$⊢x=a\to \left(\exists i\in Bi\underset{\dot{}}{+}x=n\leftrightarrow \exists i\in Bi\underset{\dot{}}{+}a=n\right)$$
37	33 36	anbi12d	$$⊢x=a\to \left(\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\leftrightarrow \left(n\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=n\right)\right)$$
38	37	rspcv	$$⊢a\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 \left(n\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=n\right)\right)$$
39		simpl	$$⊢\left(n\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=n\right)\to n\underset{\dot{}}{+}a=a$$
40	38 39	syl6com	$$⊢\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\to \left(a\in B\to n\underset{\dot{}}{+}a=a\right)$$
41	40	ad2antlr	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> ( n .+ a ) = a ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> ( n .+ a ) = a ) ) with typecode |-
42	41	imp	Could not format ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> ( n .+ a ) = a ) : No typesetting found for |- ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> ( n .+ a ) = a ) with typecode |-
43		oveq1	$$⊢i=b\to i\underset{\dot{}}{+}a=b\underset{\dot{}}{+}a$$
44	43	eqeq1d	$$⊢i=b\to \left(i\underset{\dot{}}{+}a=n\leftrightarrow b\underset{\dot{}}{+}a=n\right)$$
45	44	cbvrexvw	$$⊢\exists i\in Bi\underset{\dot{}}{+}a=n\leftrightarrow \exists b\in Bb\underset{\dot{}}{+}a=n$$
46	45	biimpi	$$⊢\exists i\in Bi\underset{\dot{}}{+}a=n\to \exists b\in Bb\underset{\dot{}}{+}a=n$$
47	46	adantl	$$⊢\left(n\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=n\right)\to \exists b\in Bb\underset{\dot{}}{+}a=n$$
48	38 47	syl6com	$$⊢\forall x\in B\left(n\underset{\dot{}}{+}x=x\wedge \exists i\in Bi\underset{\dot{}}{+}x=n\right)\to \left(a\in B\to \exists b\in Bb\underset{\dot{}}{+}a=n\right)$$
49	48	ad2antlr	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> E. b e. B ( b .+ a ) = n ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> E. b e. B ( b .+ a ) = n ) ) with typecode |-
50	49	imp	Could not format ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> E. b e. B ( b .+ a ) = n ) : No typesetting found for |- ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> E. b e. B ( b .+ a ) = n ) with typecode |-
51	22 23 27 29 30 42 50	isgrpde	Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Grp ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Grp ) with typecode |-
52	51	ex	Could not format ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) -> ( G e. Smgrp -> G e. Grp ) ) : No typesetting found for |- ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) -> ( G e. Smgrp -> G e. Grp ) ) with typecode |-
53	52	rexlimiva	Could not format ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( G e. Smgrp -> G e. Grp ) ) : 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 -> G e. Grp ) ) with typecode |-
54	53	impcom	Could not format ( ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) -> G e. Grp ) : 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 ) ) -> G e. Grp ) with typecode |-
55	21 54	impbii	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 |-