Theorem 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	|- .+ = ( +g ` M )
	cntri.z	|- Z = ( Cntr ` M )
Assertion	cntri	|- ( ( X e. Z /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step	Hyp	Ref	Expression
1		cntri.b	|- B = ( Base ` M )
2		cntri.p	|- .+ = ( +g ` 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 e. Z <-> X e. ( ( Cntz ` M ) ` B ) )
8	2 4	cntzi	|- ( ( X e. ( ( Cntz ` M ) ` B ) /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
9	7 8	sylanb	|- ( ( X e. Z /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )