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={opp}_{𝑔}\left(G\right)$$
	oppgcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
Assertion	oppgcntz	$$⊢Z\left(A\right)=\mathrm{Cntz}\left(O\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppggic.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
2		oppgcntz.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
3		eqcom	$$⊢x{+}_{G}y=y{+}_{G}x\leftrightarrow y{+}_{G}x=x{+}_{G}y$$
4		eqid	$$⊢{+}_G={+}_G$$
5		eqid	$$⊢{+}_O={+}_O$$
6	4 1 5	oppgplus	$$⊢x{+}_{O}y=y{+}_{G}x$$
7	4 1 5	oppgplus	$$⊢y{+}_{O}x=x{+}_{G}y$$
8	6 7	eqeq12i	$$⊢x{+}_{O}y=y{+}_{O}x\leftrightarrow y{+}_{G}x=x{+}_{G}y$$
9	3 8	bitr4i	$$⊢x{+}_{G}y=y{+}_{G}x\leftrightarrow x{+}_{O}y=y{+}_{O}x$$
10	9	ralbii	$$⊢\forall y\in Ax{+}_{G}y=y{+}_{G}x\leftrightarrow \forall y\in Ax{+}_{O}y=y{+}_{O}x$$
11	10	anbi2i	$$⊢\left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{G}y=y{+}_{G}x\right)\leftrightarrow \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{O}y=y{+}_{O}x\right)$$
12	11	anbi2i	$$⊢\left(A\subseteq {\mathrm{Base}}_G\wedge \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{G}y=y{+}_{G}x\right)\right)\leftrightarrow \left(A\subseteq {\mathrm{Base}}_G\wedge \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{O}y=y{+}_{O}x\right)\right)$$
13		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
14	13 2	cntzrcl	$$⊢x\in Z\left(A\right)\to \left(G\in \mathrm{V}\wedge A\subseteq {\mathrm{Base}}_G\right)$$
15	14	simprd	$$⊢x\in Z\left(A\right)\to A\subseteq {\mathrm{Base}}_G$$
16	13 4 2	elcntz	$$⊢A\subseteq {\mathrm{Base}}_G\to \left(x\in Z\left(A\right)\leftrightarrow \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{G}y=y{+}_{G}x\right)\right)$$
17	15 16	biadanii	$$⊢x\in Z\left(A\right)\leftrightarrow \left(A\subseteq {\mathrm{Base}}_G\wedge \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{G}y=y{+}_{G}x\right)\right)$$
18	1 13	oppgbas	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_O$$
19		eqid	$$⊢\mathrm{Cntz}\left(O\right)=\mathrm{Cntz}\left(O\right)$$
20	18 19	cntzrcl	$$⊢x\in \mathrm{Cntz}\left(O\right)\left(A\right)\to \left(O\in \mathrm{V}\wedge A\subseteq {\mathrm{Base}}_G\right)$$
21	20	simprd	$$⊢x\in \mathrm{Cntz}\left(O\right)\left(A\right)\to A\subseteq {\mathrm{Base}}_G$$
22	18 5 19	elcntz	$$⊢A\subseteq {\mathrm{Base}}_G\to \left(x\in \mathrm{Cntz}\left(O\right)\left(A\right)\leftrightarrow \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{O}y=y{+}_{O}x\right)\right)$$
23	21 22	biadanii	$$⊢x\in \mathrm{Cntz}\left(O\right)\left(A\right)\leftrightarrow \left(A\subseteq {\mathrm{Base}}_G\wedge \left(x\in {\mathrm{Base}}_G\wedge \forall y\in Ax{+}_{O}y=y{+}_{O}x\right)\right)$$
24	12 17 23	3bitr4i	$$⊢x\in Z\left(A\right)\leftrightarrow x\in \mathrm{Cntz}\left(O\right)\left(A\right)$$
25	24	eqriv	$$⊢Z\left(A\right)=\mathrm{Cntz}\left(O\right)\left(A\right)$$