Theorem cntri

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

	Ref	Expression
Hypotheses	cntri.b	$$⊢B={\mathrm{Base}}_M$$
	cntri.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	cntri.z	$$⊢Z=\mathrm{Cntr}\left(M\right)$$
Assertion	cntri	$$⊢\left(X\in Z\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

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