dfgrp3

Description: Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Theorem 3.2 of Bruck p. 28. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp3.b	$⊢ B = {Base}_{G}$
	dfgrp3.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	dfgrp3	$⊢ G \in Grp \leftrightarrow (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))$

Proof

Step	Hyp	Ref	Expression
1		dfgrp3.b	$⊢ B = {Base}_{G}$
2		dfgrp3.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsgrp	$⊢ G \in Grp \to G \in Smgrp$
4	1	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
5		simpl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to G \in Grp$
6		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
7	6	adantl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to y \in B$
8		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
9	8	adantl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to x \in B$
10		eqid	$⊢ -_{G} = -_{G}$
11	1 10	grpsubcl	$⊢ (G \in Grp \land y \in B \land x \in B) \to y -_{G} x \in B$
12	5 7 9 11	syl3anc	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to y -_{G} x \in B$
13		oveq1	$⊢ l = y -_{G} x \to l \underset{˙}{+} x = (y -_{G} x) \underset{˙}{+} x$
14	13	eqeq1d	$⊢ l = y -_{G} x \to (l \underset{˙}{+} x = y \leftrightarrow (y -_{G} x) \underset{˙}{+} x = y)$
15	14	adantl	$⊢ ((G \in Grp \land (x \in B \land y \in B)) \land l = y -_{G} x) \to (l \underset{˙}{+} x = y \leftrightarrow (y -_{G} x) \underset{˙}{+} x = y)$
16	1 2 10	grpnpcan	$⊢ (G \in Grp \land y \in B \land x \in B) \to (y -_{G} x) \underset{˙}{+} x = y$
17	5 7 9 16	syl3anc	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (y -_{G} x) \underset{˙}{+} x = y$
18	12 15 17	rspcedvd	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to \exists l \in B l \underset{˙}{+} x = y$
19		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
20	1 19	grpinvcl	$⊢ (G \in Grp \land x \in B) \to {inv}_{g} (G) (x) \in B$
21	20	adantrr	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to {inv}_{g} (G) (x) \in B$
22	1 2 5 21 7	grpcld	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to {inv}_{g} (G) (x) \underset{˙}{+} y \in B$
23		oveq2	$⊢ r = {inv}_{g} (G) (x) \underset{˙}{+} y \to x \underset{˙}{+} r = x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y)$
24	23	eqeq1d	$⊢ r = {inv}_{g} (G) (x) \underset{˙}{+} y \to (x \underset{˙}{+} r = y \leftrightarrow x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y) = y)$
25	24	adantl	$⊢ ((G \in Grp \land (x \in B \land y \in B)) \land r = {inv}_{g} (G) (x) \underset{˙}{+} y) \to (x \underset{˙}{+} r = y \leftrightarrow x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y) = y)$
26		eqid	$⊢ 0_{G} = 0_{G}$
27	1 2 26 19	grprinv	$⊢ (G \in Grp \land x \in B) \to x \underset{˙}{+} {inv}_{g} (G) (x) = 0_{G}$
28	27	adantrr	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to x \underset{˙}{+} {inv}_{g} (G) (x) = 0_{G}$
29	28	oveq1d	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (x \underset{˙}{+} {inv}_{g} (G) (x)) \underset{˙}{+} y = 0_{G} \underset{˙}{+} y$
30	1 2	grpass	$⊢ (G \in Grp \land (x \in B \land {inv}_{g} (G) (x) \in B \land y \in B)) \to (x \underset{˙}{+} {inv}_{g} (G) (x)) \underset{˙}{+} y = x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y)$
31	5 9 21 7 30	syl13anc	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (x \underset{˙}{+} {inv}_{g} (G) (x)) \underset{˙}{+} y = x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y)$
32		grpmnd	$⊢ G \in Grp \to G \in Mnd$
33	1 2 26	mndlid	$⊢ (G \in Mnd \land y \in B) \to 0_{G} \underset{˙}{+} y = y$
34	32 6 33	syl2an	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to 0_{G} \underset{˙}{+} y = y$
35	29 31 34	3eqtr3d	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to x \underset{˙}{+} ({inv}_{g} (G) (x) \underset{˙}{+} y) = y$
36	22 25 35	rspcedvd	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to \exists r \in B x \underset{˙}{+} r = y$
37	18 36	jca	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)$
38	37	ralrimivva	$⊢ G \in Grp \to \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)$
39	3 4 38	3jca	$⊢ G \in Grp \to (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))$
40		simp1	$⊢ (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to G \in Smgrp$
41	1 2	dfgrp3lem	$⊢ (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to \exists u \in B \forall a \in B (u \underset{˙}{+} a = a \land \exists i \in B i \underset{˙}{+} a = u)$
42	1 2	dfgrp2	$⊢ G \in Grp \leftrightarrow (G \in Smgrp \land \exists u \in B \forall a \in B (u \underset{˙}{+} a = a \land \exists i \in B i \underset{˙}{+} a = u))$
43	40 41 42	sylanbrc	$⊢ (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to G \in Grp$
44	39 43	impbii	$⊢ G \in Grp \leftrightarrow (G \in Smgrp \land B \neq \emptyset \land \forall x \in B \forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))$

Metamath Proof Explorer

Theorem dfgrp3

Proof