Theorem cntzel

Description: Membership in a centralizer. (Contributed by Stefan O'Rear, 6-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	cntzel	$$⊢\left(S\subseteq B\wedge X\in B\right)\to \left(X\in Z\left(S\right)\leftrightarrow \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\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	elcntz	$$⊢S\subseteq B\to \left(X\in Z\left(S\right)\leftrightarrow \left(X\in B\wedge \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\right)\right)$$
5	4	baibd	$$⊢\left(S\subseteq B\wedge X\in B\right)\to \left(X\in Z\left(S\right)\leftrightarrow \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\right)$$