Theorem mgm2mgm

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

	Ref	Expression
Assertion	mgm2mgm	$$⊢M\in \mathrm{MgmALT}\leftrightarrow M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
2		eqid	$$⊢{+}_M={+}_M$$
3	1 2	ismgmALT	$$⊢M\in \mathrm{MgmALT}\to \left(M\in \mathrm{MgmALT}\leftrightarrow {+}_M\mathrm{clLaw}{\mathrm{Base}}_M\right)$$
4		fvex	$$⊢{+}_M\in \mathrm{V}$$
5		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
6		iscllaw	$$⊢\left({+}_M\in \mathrm{V}\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)\to \left({+}_M\mathrm{clLaw}{\mathrm{Base}}_M\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M\right)$$
7	4 5 6	mp2an	$$⊢{+}_M\mathrm{clLaw}{\mathrm{Base}}_M\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M$$
8	1 2	ismgm	$$⊢M\in \mathrm{MgmALT}\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M\right)$$
9	8	biimprd	$$⊢M\in \mathrm{MgmALT}\to \left(\forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M\to M\in \mathrm{Mgm}\right)$$
10	7 9	biimtrid	$$⊢M\in \mathrm{MgmALT}\to \left({+}_M\mathrm{clLaw}{\mathrm{Base}}_M\to M\in \mathrm{Mgm}\right)$$
11	3 10	sylbid	$$⊢M\in \mathrm{MgmALT}\to \left(M\in \mathrm{MgmALT}\to M\in \mathrm{Mgm}\right)$$
12	11	pm2.43i	$$⊢M\in \mathrm{MgmALT}\to M\in \mathrm{Mgm}$$
13		mgmplusgiopALT	$$⊢M\in \mathrm{Mgm}\to {+}_M\mathrm{clLaw}{\mathrm{Base}}_M$$
14	1 2	ismgmALT	$$⊢M\in \mathrm{Mgm}\to \left(M\in \mathrm{MgmALT}\leftrightarrow {+}_M\mathrm{clLaw}{\mathrm{Base}}_M\right)$$
15	13 14	mpbird	$$⊢M\in \mathrm{Mgm}\to M\in \mathrm{MgmALT}$$
16	12 15	impbii	$$⊢M\in \mathrm{MgmALT}\leftrightarrow M\in \mathrm{Mgm}$$