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=opp𝑔G
oppgcntr.z Z=CntrG
Assertion oppgcntr Z=CntrO

Proof

Step Hyp Ref Expression
1 oppggic.o O=opp𝑔G
2 oppgcntr.z Z=CntrG
3 eqid CntzG=CntzG
4 1 3 oppgcntz CntzGBaseG=CntzOBaseG
5 eqid BaseG=BaseG
6 5 3 cntrval CntzGBaseG=CntrG
7 6 2 eqtr4i CntzGBaseG=Z
8 1 5 oppgbas BaseG=BaseO
9 eqid CntzO=CntzO
10 8 9 cntrval CntzOBaseG=CntrO
11 4 7 10 3eqtr3i Z=CntrO