Theorem iscmn

Description: The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	iscmn.b	$$⊢B={\mathrm{Base}}_G$$
	iscmn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	iscmn	$$⊢G\in \mathrm{CMnd}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscmn.b	$$⊢B={\mathrm{Base}}_G$$
2		iscmn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
4	3 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
5		raleq	$$⊢{\mathrm{Base}}_g=B\to \left(\forall y\in {\mathrm{Base}}_{g}x{+}_{g}y=y{+}_{g}x\leftrightarrow \forall y\in Bx{+}_{g}y=y{+}_{g}x\right)$$
6	5	raleqbi1dv	$$⊢{\mathrm{Base}}_g=B\to \left(\forall x\in {\mathrm{Base}}_g\forall y\in {\mathrm{Base}}_{g}x{+}_{g}y=y{+}_{g}x\leftrightarrow \forall x\in B\forall y\in Bx{+}_{g}y=y{+}_{g}x\right)$$
7	4 6	syl	$$⊢g=G\to \left(\forall x\in {\mathrm{Base}}_g\forall y\in {\mathrm{Base}}_{g}x{+}_{g}y=y{+}_{g}x\leftrightarrow \forall x\in B\forall y\in Bx{+}_{g}y=y{+}_{g}x\right)$$
8		fveq2	$$⊢g=G\to {+}_g={+}_G$$
9	8 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
10	9	oveqd	$$⊢g=G\to x{+}_{g}y=x\underset{\dot{}}{+}y$$
11	9	oveqd	$$⊢g=G\to y{+}_{g}x=y\underset{\dot{}}{+}x$$
12	10 11	eqeq12d	$$⊢g=G\to \left(x{+}_{g}y=y{+}_{g}x\leftrightarrow x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
13	12	2ralbidv	$$⊢g=G\to \left(\forall x\in B\forall y\in Bx{+}_{g}y=y{+}_{g}x\leftrightarrow \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
14	7 13	bitrd	$$⊢g=G\to \left(\forall x\in {\mathrm{Base}}_g\forall y\in {\mathrm{Base}}_{g}x{+}_{g}y=y{+}_{g}x\leftrightarrow \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
15		df-cmn	$$⊢\mathrm{CMnd}=\left\{g\in \mathrm{Mnd}|\forall x\in {\mathrm{Base}}_g\forall y\in {\mathrm{Base}}_{g}x{+}_{g}y=y{+}_{g}x\right\}$$
16	14 15	elrab2	$$⊢G\in \mathrm{CMnd}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$