This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isabli

Description: Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		isabli.g	$⊢ G \in Grp$
2		isabli.b	$⊢ B = {Base}_{G}$
3		isabli.p	$⊢ \underset{˙}{+} = +_{G}$
4		isabli.c	$⊢ (x \in B \land y \in B) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
5	4	rgen2	$⊢ \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x$
6	2 3	isabl2	$⊢ G \in Abel \leftrightarrow (G \in Grp \land \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$
7	1 5 6	mpbir2an	$⊢ G \in Abel$