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 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
oppgcntr.z ⊢ 𝑍 = ( Cntr ‘ 𝐺 )
Assertion oppgcntr 𝑍 = ( Cntr ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 oppgcntr.z ⊢ 𝑍 = ( Cntr ‘ 𝐺 )
3 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
4 1 3 oppgcntz ⊢ ( ( Cntz ‘ 𝐺 ) ‘ ( Base ‘ 𝐺 ) ) = ( ( Cntz ‘ 𝑂 ) ‘ ( Base ‘ 𝐺 ) )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 3 cntrval ⊢ ( ( Cntz ‘ 𝐺 ) ‘ ( Base ‘ 𝐺 ) ) = ( Cntr ‘ 𝐺 )
7 6 2 eqtr4i ⊢ ( ( Cntz ‘ 𝐺 ) ‘ ( Base ‘ 𝐺 ) ) = 𝑍
8 1 5 oppgbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
9 eqid ⊢ ( Cntz ‘ 𝑂 ) = ( Cntz ‘ 𝑂 )
10 8 9 cntrval ⊢ ( ( Cntz ‘ 𝑂 ) ‘ ( Base ‘ 𝐺 ) ) = ( Cntr ‘ 𝑂 )
11 4 7 10 3eqtr3i ⊢ 𝑍 = ( Cntr ‘ 𝑂 )