Metamath Proof Explorer

Theorem iscmnd

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

		Ref	Expression
	Hypotheses	iscmnd.b	$⊢ φ \to B = {Base}_{G}$
		iscmnd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
		iscmnd.g	$⊢ φ \to G \in Mnd$
		iscmnd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
	Assertion	iscmnd	$⊢ φ \to G \in CMnd$

Proof

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