Theorem issgrpd

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

	Ref	Expression
Hypotheses	issgrpd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	issgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	issgrpd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	issgrpd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
	issgrpd.v	$$⊢\phi \to G\in V$$
Assertion	issgrpd	Could not format assertion : No typesetting found for |- ( ph -> G e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		issgrpd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		issgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		issgrpd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
4		issgrpd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
5		issgrpd.v	$$⊢\phi \to G\in V$$
6	3	3expib	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B\right)$$
7	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_G\right)$$
8	1	eleq2d	$$⊢\phi \to \left(y\in B\leftrightarrow y\in {\mathrm{Base}}_G\right)$$
9	7 8	anbi12d	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\leftrightarrow \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)$$
10	2	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{G}y$$
11	10 1	eleq12d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow x{+}_{G}y\in {\mathrm{Base}}_G\right)$$
12	6 9 11	3imtr3d	$$⊢\phi \to \left(\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to x{+}_{G}y\in {\mathrm{Base}}_G\right)$$
13	12	imp	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y\in {\mathrm{Base}}_G$$
14		df-3an	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\leftrightarrow \left(\left(x\in B\wedge y\in B\right)\wedge z\in B\right)$$
15	14 4	sylan2br	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge y\in B\right)\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
16	15	ex	$$⊢\phi \to \left(\left(\left(x\in B\wedge y\in B\right)\wedge z\in B\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)$$
17	1	eleq2d	$$⊢\phi \to \left(z\in B\leftrightarrow z\in {\mathrm{Base}}_G\right)$$
18	9 17	anbi12d	$$⊢\phi \to \left(\left(\left(x\in B\wedge y\in B\right)\wedge z\in B\right)\leftrightarrow \left(\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\wedge z\in {\mathrm{Base}}_G\right)\right)$$
19		eqidd	$$⊢\phi \to z=z$$
20	2 10 19	oveq123d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=\left(x{+}_{G}y\right){+}_{G}z$$
21		eqidd	$$⊢\phi \to x=x$$
22	2	oveqd	$$⊢\phi \to y\underset{\dot{}}{+}z=y{+}_{G}z$$
23	2 21 22	oveq123d	$$⊢\phi \to x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)=x{+}_G\left(y{+}_{G}z\right)$$
24	20 23	eqeq12d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\leftrightarrow \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
25	16 18 24	3imtr3d	$$⊢\phi \to \left(\left(\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\wedge z\in {\mathrm{Base}}_G\right)\to \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
26	25	impl	$$⊢\left(\left(\phi \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\wedge z\in {\mathrm{Base}}_G\right)\to \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)$$
27	26	ralrimiva	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)$$
28	13 27	jca	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to \left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
29	28	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
30		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
31		eqid	$$⊢{+}_G={+}_G$$
32	30 31	issgrpv	Could not format ( G e. V -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) ) : No typesetting found for |- ( G e. V -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) ) with typecode |-
33	5 32	syl	Could not format ( ph -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) ) : No typesetting found for |- ( ph -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) ) with typecode |-
34	29 33	mpbird	Could not format ( ph -> G e. Smgrp ) : No typesetting found for |- ( ph -> G e. Smgrp ) with typecode |-