Theorem sgrp2sgrp

Description: Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020)

	Ref	Expression
Assertion	sgrp2sgrp	Could not format assertion : No typesetting found for |- ( M e. SGrpALT <-> M e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgm2mgm	$$⊢M\in \mathrm{MgmALT}\leftrightarrow M\in \mathrm{Mgm}$$
2	1	anbi1i	$$⊢\left(M\in \mathrm{MgmALT}\wedge {+}_M\mathrm{assLaw}{\mathrm{Base}}_M\right)\leftrightarrow \left(M\in \mathrm{Mgm}\wedge {+}_M\mathrm{assLaw}{\mathrm{Base}}_M\right)$$
3		fvex	$$⊢{+}_M\in \mathrm{V}$$
4		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
5	3 4	pm3.2i	$$⊢\left({+}_M\in \mathrm{V}\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)$$
6		isasslaw	$$⊢\left({+}_M\in \mathrm{V}\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)\to \left({+}_M\mathrm{assLaw}{\mathrm{Base}}_M\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)\right)$$
7	5 6	mp1i	$$⊢M\in \mathrm{Mgm}\to \left({+}_M\mathrm{assLaw}{\mathrm{Base}}_M\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)\right)$$
8	7	pm5.32i	$$⊢\left(M\in \mathrm{Mgm}\wedge {+}_M\mathrm{assLaw}{\mathrm{Base}}_M\right)\leftrightarrow \left(M\in \mathrm{Mgm}\wedge \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)\right)$$
9	2 8	bitri	$$⊢\left(M\in \mathrm{MgmALT}\wedge {+}_M\mathrm{assLaw}{\mathrm{Base}}_M\right)\leftrightarrow \left(M\in \mathrm{Mgm}\wedge \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
11		eqid	$$⊢{+}_M={+}_M$$
12	10 11	issgrpALT	$$⊢M\in \mathrm{SGrpALT}\leftrightarrow \left(M\in \mathrm{MgmALT}\wedge {+}_M\mathrm{assLaw}{\mathrm{Base}}_M\right)$$
13	10 11	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) with typecode |-
14	9 12 13	3bitr4i	Could not format ( M e. SGrpALT <-> M e. Smgrp ) : No typesetting found for |- ( M e. SGrpALT <-> M e. Smgrp ) with typecode |-