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	$⊢ \underset{˙}{+} = +_{G}$
Assertion	dfgrp2	$⊢ G \in Grp \leftrightarrow (G \in Smgrp \land \exists n \in B \forall x \in B (n \underset{˙}{+} x = x \land \exists i \in B i \underset{˙}{+} x = n))$

Proof

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

Metamath Proof Explorer

Theorem dfgrp2

Proof