Metamath Proof Explorer

Theorem oppgcntz

Description: A centralizer in a group is the same as the centralizer in the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses oppggic.o 
|- O = ( oppG ` G )
oppgcntz.z 
|- Z = ( Cntz ` G )
Assertion oppgcntz 
|- ( Z ` A ) = ( ( Cntz ` O ) ` A )

Proof

Step Hyp Ref Expression
1 oppggic.o 
 |-  O = ( oppG ` G )
2 oppgcntz.z 
 |-  Z = ( Cntz ` G )
3 eqcom 
 |-  ( ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( y ( +g ` G ) x ) = ( x ( +g ` G ) y ) )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 eqid 
 |-  ( +g ` O ) = ( +g ` O )
6 4 1 5 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` G ) x )
7 4 1 5 oppgplus 
 |-  ( y ( +g ` O ) x ) = ( x ( +g ` G ) y )
8 6 7 eqeq12i 
 |-  ( ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) <-> ( y ( +g ` G ) x ) = ( x ( +g ` G ) y ) )
9 3 8 bitr4i 
 |-  ( ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) )
10 9 ralbii 
 |-  ( A. y e. A ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> A. y e. A ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) )
11 10 anbi2i 
 |-  ( ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) <-> ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) ) )
12 11 anbi2i 
 |-  ( ( A C_ ( Base ` G ) /\ ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) <-> ( A C_ ( Base ` G ) /\ ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) ) ) )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 13 2 cntzrcl 
 |-  ( x e. ( Z ` A ) -> ( G e. _V /\ A C_ ( Base ` G ) ) )
15 14 simprd 
 |-  ( x e. ( Z ` A ) -> A C_ ( Base ` G ) )
16 13 4 2 elcntz 
 |-  ( A C_ ( Base ` G ) -> ( x e. ( Z ` A ) <-> ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
17 15 16 biadanii 
 |-  ( x e. ( Z ` A ) <-> ( A C_ ( Base ` G ) /\ ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
18 1 13 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
19 eqid 
 |-  ( Cntz ` O ) = ( Cntz ` O )
20 18 19 cntzrcl 
 |-  ( x e. ( ( Cntz ` O ) ` A ) -> ( O e. _V /\ A C_ ( Base ` G ) ) )
21 20 simprd 
 |-  ( x e. ( ( Cntz ` O ) ` A ) -> A C_ ( Base ` G ) )
22 18 5 19 elcntz 
 |-  ( A C_ ( Base ` G ) -> ( x e. ( ( Cntz ` O ) ` A ) <-> ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) ) ) )
23 21 22 biadanii 
 |-  ( x e. ( ( Cntz ` O ) ` A ) <-> ( A C_ ( Base ` G ) /\ ( x e. ( Base ` G ) /\ A. y e. A ( x ( +g ` O ) y ) = ( y ( +g ` O ) x ) ) ) )
24 12 17 23 3bitr4i 
 |-  ( x e. ( Z ` A ) <-> x e. ( ( Cntz ` O ) ` A ) )
25 24 eqriv 
 |-  ( Z ` A ) = ( ( Cntz ` O ) ` A )