Theorem cntzsnval

Description: Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-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	cntzsnval	$$⊢Y\in B\to Z\left(\left\{Y\right\}\right)=\left\{x\in B|x\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		snssi	$$⊢Y\in B\to \left\{Y\right\}\subseteq B$$
5	1 2 3	cntzval	$$⊢\left\{Y\right\}\subseteq B\to Z\left(\left\{Y\right\}\right)=\left\{x\in B|\forall y\in \left\{Y\right\}x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
6	4 5	syl	$$⊢Y\in B\to Z\left(\left\{Y\right\}\right)=\left\{x\in B|\forall y\in \left\{Y\right\}x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
7		oveq2	$$⊢y=Y\to x\underset{\dot{}}{+}y=x\underset{\dot{}}{+}Y$$
8		oveq1	$$⊢y=Y\to y\underset{\dot{}}{+}x=Y\underset{\dot{}}{+}x$$
9	7 8	eqeq12d	$$⊢y=Y\to \left(x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right)$$
10	9	ralsng	$$⊢Y\in B\to \left(\forall y\in \left\{Y\right\}x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right)$$
11	10	rabbidv	$$⊢Y\in B\to \left\{x\in B|\forall y\in \left\{Y\right\}x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}=\left\{x\in B|x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right\}$$
12	6 11	eqtrd	$$⊢Y\in B\to Z\left(\left\{Y\right\}\right)=\left\{x\in B|x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right\}$$