dfgrp3e

Description: Alternate definition of a group as a set with a closed, associative operation, for which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Exercise 1 of Herstein p. 57. (Contributed by NM, 5-Dec-2006) (Revised by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp3.b	$⊢ B = {Base}_{G}$
	dfgrp3.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	dfgrp3e	$⊢ G \in Grp \leftrightarrow (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\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	1 2	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))$
4		simp2	$⊢ (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 B \neq \emptyset$
5		sgrpmgm	$⊢ G \in Smgrp \to G \in Mgm$
6	5	adantr	$⊢ (G \in Smgrp \land x \in B) \to G \in Mgm$
7	6	adantr	$⊢ ((G \in Smgrp \land x \in B) \land y \in B) \to G \in Mgm$
8		simpr	$⊢ (G \in Smgrp \land x \in B) \to x \in B$
9	8	adantr	$⊢ ((G \in Smgrp \land x \in B) \land y \in B) \to x \in B$
10		simpr	$⊢ ((G \in Smgrp \land x \in B) \land y \in B) \to y \in B$
11	1 2	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
12	7 9 10 11	syl3anc	$⊢ ((G \in Smgrp \land x \in B) \land y \in B) \to x \underset{˙}{+} y \in B$
13	12	adantr	$⊢ (((G \in Smgrp \land x \in B) \land y \in B) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to x \underset{˙}{+} y \in B$
14	1 2	sgrpass	$⊢ (G \in Smgrp \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
15	14	3anassrs	$⊢ (((G \in Smgrp \land x \in B) \land y \in B) \land z \in B) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
16	15	ralrimiva	$⊢ ((G \in Smgrp \land x \in B) \land y \in B) \to \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
17	16	adantr	$⊢ (((G \in Smgrp \land x \in B) \land y \in B) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
18		simpr	$⊢ (((G \in Smgrp \land x \in B) \land y \in B) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)$
19	13 17 18	3jca	$⊢ (((G \in Smgrp \land x \in B) \land y \in B) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))$
20	19	ex	$⊢ ((G \in Smgrp \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) \to (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$
21	20	ralimdva	$⊢ (G \in Smgrp \land x \in B) \to (\forall y \in B (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y) \to \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$
22	21	ralimdva	$⊢ G \in Smgrp \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) \to \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$
23	22	a1d	$⊢ G \in Smgrp \to (B \neq \emptyset \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) \to \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))))$
24	23	3imp	$⊢ (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 \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))$
25	4 24	jca	$⊢ (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 (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$
26		n0	$⊢ B \neq \emptyset \leftrightarrow \exists a a \in B$
27		3simpa	$⊢ (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z))$
28	27	2ralimi	$⊢ \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z))$
29	1 2	issgrpn0	$⊢ a \in B \to (G \in Smgrp \leftrightarrow \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)))$
30	28 29	imbitrrid	$⊢ a \in B \to (\forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to G \in Smgrp)$
31	30	exlimiv	$⊢ \exists a a \in B \to (\forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to G \in Smgrp)$
32	26 31	sylbi	$⊢ B \neq \emptyset \to (\forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to G \in Smgrp)$
33	32	imp	$⊢ (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))) \to G \in Smgrp$
34		simpl	$⊢ (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))) \to B \neq \emptyset$
35		simp3	$⊢ (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \to (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)$
36	35	2ralimi	$⊢ \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)) \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)$
37	36	adantl	$⊢ (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))) \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)$
38	33 34 37	3jca	$⊢ (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y))) \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))$
39	25 38	impbii	$⊢ (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)) \leftrightarrow (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$
40	3 39	bitri	$⊢ G \in Grp \leftrightarrow (B \neq \emptyset \land \forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \land (\exists l \in B l \underset{˙}{+} x = y \land \exists r \in B x \underset{˙}{+} r = y)))$

Metamath Proof Explorer

Theorem dfgrp3e

Proof