Theorem elcntz

Description: Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
	cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	elcntz	$$⊢S\subseteq B\to \left(A\in Z\left(S\right)\leftrightarrow \left(A\in B\wedge \forall y\in SA\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
3		cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
4	1 2 3	cntzval	$$⊢S\subseteq B\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
5	4	eleq2d	$$⊢S\subseteq B\to \left(A\in Z\left(S\right)\leftrightarrow A\in \left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
6		oveq1	$$⊢x=A\to x\underset{\dot{}}{+}y=A\underset{\dot{}}{+}y$$
7		oveq2	$$⊢x=A\to y\underset{\dot{}}{+}x=y\underset{\dot{}}{+}A$$
8	6 7	eqeq12d	$$⊢x=A\to \left(x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow A\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)$$
9	8	ralbidv	$$⊢x=A\to \left(\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow \forall y\in SA\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)$$
10	9	elrab	$$⊢A\in \left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\leftrightarrow \left(A\in B\wedge \forall y\in SA\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)$$
11	5 10	bitrdi	$$⊢S\subseteq B\to \left(A\in Z\left(S\right)\leftrightarrow \left(A\in B\wedge \forall y\in SA\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)\right)$$