issgrpd

Description: Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	issgrpd.b	$⊢ φ \to B = {Base}_{G}$
	issgrpd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
	issgrpd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
	issgrpd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	issgrpd.v	$⊢ φ \to G \in V$
Assertion	issgrpd	$⊢ φ \to G \in Smgrp$

Proof

Step	Hyp	Ref	Expression
1		issgrpd.b	$⊢ φ \to B = {Base}_{G}$
2		issgrpd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		issgrpd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
4		issgrpd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
5		issgrpd.v	$⊢ φ \to G \in V$
6	3	3expib	$⊢ φ \to ((x \in B \land y \in B) \to x \underset{˙}{+} y \in B)$
7	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{G})$
8	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{G})$
9	7 8	anbi12d	$⊢ φ \to ((x \in B \land y \in B) \leftrightarrow (x \in {Base}_{G} \land y \in {Base}_{G}))$
10	2	oveqd	$⊢ φ \to x \underset{˙}{+} y = x +_{G} y$
11	10 1	eleq12d	$⊢ φ \to (x \underset{˙}{+} y \in B \leftrightarrow x +_{G} y \in {Base}_{G})$
12	6 9 11	3imtr3d	$⊢ φ \to ((x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y \in {Base}_{G})$
13	12	imp	$⊢ (φ \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to x +_{G} y \in {Base}_{G}$
14		df-3an	$⊢ (x \in B \land y \in B \land z \in B) \leftrightarrow ((x \in B \land y \in B) \land z \in B)$
15	14 4	sylan2br	$⊢ (φ \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	ex	$⊢ φ \to (((x \in B \land y \in B) \land z \in B) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z))$
17	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{G})$
18	9 17	anbi12d	$⊢ φ \to (((x \in B \land y \in B) \land z \in B) \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land z \in {Base}_{G}))$
19		eqidd	$⊢ φ \to z = z$
20	2 10 19	oveq123d	$⊢ φ \to (x \underset{˙}{+} y) \underset{˙}{+} z = (x +_{G} y) +_{G} z$
21		eqidd	$⊢ φ \to x = x$
22	2	oveqd	$⊢ φ \to y \underset{˙}{+} z = y +_{G} z$
23	2 21 22	oveq123d	$⊢ φ \to x \underset{˙}{+} (y \underset{˙}{+} z) = x +_{G} (y +_{G} z)$
24	20 23	eqeq12d	$⊢ φ \to ((x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z) \leftrightarrow (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z))$
25	16 18 24	3imtr3d	$⊢ φ \to (((x \in {Base}_{G} \land y \in {Base}_{G}) \land z \in {Base}_{G}) \to (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z))$
26	25	impl	$⊢ ((φ \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land z \in {Base}_{G}) \to (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z)$
27	26	ralrimiva	$⊢ (φ \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to \forall z \in {Base}_{G} (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z)$
28	13 27	jca	$⊢ (φ \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (x +_{G} y \in {Base}_{G} \land \forall z \in {Base}_{G} (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z))$
29	28	ralrimivva	$⊢ φ \to \forall x \in {Base}_{G} \forall y \in {Base}_{G} (x +_{G} y \in {Base}_{G} \land \forall z \in {Base}_{G} (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z))$
30		eqid	$⊢ {Base}_{G} = {Base}_{G}$
31		eqid	$⊢ +_{G} = +_{G}$
32	30 31	issgrpv	$⊢ G \in V \to (G \in Smgrp \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (x +_{G} y \in {Base}_{G} \land \forall z \in {Base}_{G} (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z)))$
33	5 32	syl	$⊢ φ \to (G \in Smgrp \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (x +_{G} y \in {Base}_{G} \land \forall z \in {Base}_{G} (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z)))$
34	29 33	mpbird	$⊢ φ \to G \in Smgrp$

Metamath Proof Explorer

Theorem issgrpd

Proof