cntri

Description: Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	cntri.b	$⊢ B = {Base}_{M}$
	cntri.p	$⊢ \underset{˙}{+} = +_{M}$
	cntri.z	$⊢ Z = Cntr (M)$
Assertion	cntri	$⊢ (X \in Z \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Step	Hyp	Ref	Expression
1		cntri.b	$⊢ B = {Base}_{M}$
2		cntri.p	$⊢ \underset{˙}{+} = +_{M}$
3		cntri.z	$⊢ Z = Cntr (M)$
4		eqid	$⊢ Cntz (M) = Cntz (M)$
5	1 4	cntrval	$⊢ Cntz (M) (B) = Cntr (M)$
6	3 5	eqtr4i	$⊢ Z = Cntz (M) (B)$
7	6	eleq2i	$⊢ X \in Z \leftrightarrow X \in Cntz (M) (B)$
8	2 4	cntzi	$⊢ (X \in Cntz (M) (B) \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
9	7 8	sylanb	$⊢ (X \in Z \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer