Metamath Proof Explorer


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 ) )