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 = ( Base ` G )
	dfgrp2.p	\|- .+ = ( +g ` G )
Assertion	dfgrp2	\|- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )

Proof

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

Metamath Proof Explorer

Theorem dfgrp2

Proof