Theorem cntziinsn

Description: Express any centralizer as an intersection of singleton 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	cntziinsn	$$⊢S\subseteq B\to Z\left(S\right)=B\cap \bigcap _{x\in S}Z\left(\left\{x\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzrec.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		eqid	$$⊢{+}_M={+}_M$$
4	1 3 2	cntzval	$$⊢S\subseteq B\to Z\left(S\right)=\left\{y\in B|\forall x\in Sy{+}_{M}x=x{+}_{M}y\right\}$$
5		ssel2	$$⊢\left(S\subseteq B\wedge x\in S\right)\to x\in B$$
6	1 3 2	cntzsnval	$$⊢x\in B\to Z\left(\left\{x\right\}\right)=\left\{y\in B|y{+}_{M}x=x{+}_{M}y\right\}$$
7	5 6	syl	$$⊢\left(S\subseteq B\wedge x\in S\right)\to Z\left(\left\{x\right\}\right)=\left\{y\in B|y{+}_{M}x=x{+}_{M}y\right\}$$
8	7	iineq2dv	$$⊢S\subseteq B\to \bigcap _{x\in S}Z\left(\left\{x\right\}\right)=\bigcap _{x\in S}\left\{y\in B|y{+}_{M}x=x{+}_{M}y\right\}$$
9	8	ineq2d	$$⊢S\subseteq B\to B\cap \bigcap _{x\in S}Z\left(\left\{x\right\}\right)=B\cap \bigcap _{x\in S}\left\{y\in B|y{+}_{M}x=x{+}_{M}y\right\}$$
10		riinrab	$$⊢B\cap \bigcap _{x\in S}\left\{y\in B|y{+}_{M}x=x{+}_{M}y\right\}=\left\{y\in B|\forall x\in Sy{+}_{M}x=x{+}_{M}y\right\}$$
11	9 10	eqtrdi	$$⊢S\subseteq B\to B\cap \bigcap _{x\in S}Z\left(\left\{x\right\}\right)=\left\{y\in B|\forall x\in Sy{+}_{M}x=x{+}_{M}y\right\}$$
12	4 11	eqtr4d	$$⊢S\subseteq B\to Z\left(S\right)=B\cap \bigcap _{x\in S}Z\left(\left\{x\right\}\right)$$