Theorem cntzrec

Description: Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzrec.b	$$⊢B={\mathrm{Base}}_M$$
	cntzrec.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntzrec	$$⊢\left(S\subseteq B\wedge T\subseteq B\right)\to \left(S\subseteq Z\left(T\right)\leftrightarrow T\subseteq Z\left(S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzrec.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		ralcom	$$⊢\forall x\in S\forall y\in Tx{+}_{M}y=y{+}_{M}x\leftrightarrow \forall y\in T\forall x\in Sx{+}_{M}y=y{+}_{M}x$$
4		eqcom	$$⊢x{+}_{M}y=y{+}_{M}x\leftrightarrow y{+}_{M}x=x{+}_{M}y$$
5	4	2ralbii	$$⊢\forall y\in T\forall x\in Sx{+}_{M}y=y{+}_{M}x\leftrightarrow \forall y\in T\forall x\in Sy{+}_{M}x=x{+}_{M}y$$
6	3 5	bitri	$$⊢\forall x\in S\forall y\in Tx{+}_{M}y=y{+}_{M}x\leftrightarrow \forall y\in T\forall x\in Sy{+}_{M}x=x{+}_{M}y$$
7	6	a1i	$$⊢\left(S\subseteq B\wedge T\subseteq B\right)\to \left(\forall x\in S\forall y\in Tx{+}_{M}y=y{+}_{M}x\leftrightarrow \forall y\in T\forall x\in Sy{+}_{M}x=x{+}_{M}y\right)$$
8		eqid	$$⊢{+}_M={+}_M$$
9	1 8 2	sscntz	$$⊢\left(S\subseteq B\wedge T\subseteq B\right)\to \left(S\subseteq Z\left(T\right)\leftrightarrow \forall x\in S\forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
10	1 8 2	sscntz	$$⊢\left(T\subseteq B\wedge S\subseteq B\right)\to \left(T\subseteq Z\left(S\right)\leftrightarrow \forall y\in T\forall x\in Sy{+}_{M}x=x{+}_{M}y\right)$$
11	10	ancoms	$$⊢\left(S\subseteq B\wedge T\subseteq B\right)\to \left(T\subseteq Z\left(S\right)\leftrightarrow \forall y\in T\forall x\in Sy{+}_{M}x=x{+}_{M}y\right)$$
12	7 9 11	3bitr4d	$$⊢\left(S\subseteq B\wedge T\subseteq B\right)\to \left(S\subseteq Z\left(T\right)\leftrightarrow T\subseteq Z\left(S\right)\right)$$