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 )