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 ‘ 𝑂 )