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

Metamath Proof Explorer

Theorem oppgcntr

Description: The center of a group is the same as the center of the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses oppggic.o 
|- O = ( oppG ` G )
oppgcntr.z 
|- Z = ( Cntr ` G )
Assertion oppgcntr 
|- Z = ( Cntr ` O )

Proof

Step Hyp Ref Expression
1 oppggic.o 
 |-  O = ( oppG ` G )
2 oppgcntr.z 
 |-  Z = ( Cntr ` G )
3 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
4 1 3 oppgcntz 
 |-  ( ( Cntz ` G ) ` ( Base ` G ) ) = ( ( Cntz ` O ) ` ( Base ` G ) )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 3 cntrval 
 |-  ( ( Cntz ` G ) ` ( Base ` G ) ) = ( Cntr ` G )
7 6 2 eqtr4i 
 |-  ( ( Cntz ` G ) ` ( Base ` G ) ) = Z
8 1 5 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
9 eqid 
 |-  ( Cntz ` O ) = ( Cntz ` O )
10 8 9 cntrval 
 |-  ( ( Cntz ` O ) ` ( Base ` G ) ) = ( Cntr ` O )
11 4 7 10 3eqtr3i 
 |-  Z = ( Cntr ` O )