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

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 oppgcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3 eqcom ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
6 4 1 5 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 )
7 4 1 5 oppgplus ⊢ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 )
8 6 7 eqeq12i ⊢ ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9 3 8 bitr4i ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) )
10 9 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) )
11 10 anbi2i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) ) )
12 11 anbi2i ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) ) ) )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 13 2 cntzrcl ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝐴 ) → ( 𝐺 ∈ V ∧ 𝐴 ⊆ ( Base ‘ 𝐺 ) ) )
15 14 simprd ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝐴 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
16 13 4 2 elcntz ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝐴 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
17 15 16 biadanii ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝐴 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
18 1 13 oppgbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
19 eqid ⊢ ( Cntz ‘ 𝑂 ) = ( Cntz ‘ 𝑂 )
20 18 19 cntzrcl ⊢ ( 𝑥 ∈ ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 ) → ( 𝑂 ∈ V ∧ 𝐴 ⊆ ( Base ‘ 𝐺 ) ) )
21 20 simprd ⊢ ( 𝑥 ∈ ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
22 18 5 19 elcntz ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) ) ) )
23 21 22 biadanii ⊢ ( 𝑥 ∈ ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) ) ) )
24 12 17 23 3bitr4i ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝐴 ) ↔ 𝑥 ∈ ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 ) )
25 24 eqriv ⊢ ( 𝑍 ‘ 𝐴 ) = ( ( Cntz ‘ 𝑂 ) ‘ 𝐴 )