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 = opp 𝑔 ⁡ G
oppgcntr.z ⊢ Z = Cntr ⁡ G
Assertion oppgcntr ⊢ Z = Cntr ⁡ O

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ O = opp 𝑔 ⁡ 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