Theorem iscmnd

Description: Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	iscmnd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	iscmnd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	iscmnd.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	iscmnd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
Assertion	iscmnd	$$⊢\phi \to G\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		iscmnd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		iscmnd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		iscmnd.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		iscmnd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
5	4	3expib	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
6	5	ralrimivv	$$⊢\phi \to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
7	2	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{G}y$$
8	2	oveqd	$$⊢\phi \to y\underset{\dot{}}{+}x=y{+}_{G}x$$
9	7 8	eqeq12d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow x{+}_{G}y=y{+}_{G}x\right)$$
10	1 9	raleqbidv	$$⊢\phi \to \left(\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow \forall y\in {\mathrm{Base}}_{G}x{+}_{G}y=y{+}_{G}x\right)$$
11	1 10	raleqbidv	$$⊢\phi \to \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_{G}x{+}_{G}y=y{+}_{G}x\right)$$
12	11	anbi2d	$$⊢\phi \to \left(\left(G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_{G}x{+}_{G}y=y{+}_{G}x\right)\right)$$
13	3 6 12	mpbi2and	$$⊢\phi \to \left(G\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_{G}x{+}_{G}y=y{+}_{G}x\right)$$
14		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
15		eqid	$$⊢{+}_G={+}_G$$
16	14 15	iscmn	$$⊢G\in \mathrm{CMnd}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_{G}x{+}_{G}y=y{+}_{G}x\right)$$
17	13 16	sylibr	$$⊢\phi \to G\in \mathrm{CMnd}$$