Theorem cntzssv

Description: The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrcl.b	$$⊢B={\mathrm{Base}}_M$$
	cntzrcl.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntzssv	$$⊢Z\left(S\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		cntzrcl.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzrcl.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		0ss	$$⊢\varnothing \subseteq B$$
4		sseq1	$$⊢Z\left(S\right)=\varnothing \to \left(Z\left(S\right)\subseteq B\leftrightarrow \varnothing \subseteq B\right)$$
5	3 4	mpbiri	$$⊢Z\left(S\right)=\varnothing \to Z\left(S\right)\subseteq B$$
6		n0	$$⊢Z\left(S\right)\ne \varnothing \leftrightarrow \exists xx\in Z\left(S\right)$$
7	1 2	cntzrcl	$$⊢x\in Z\left(S\right)\to \left(M\in \mathrm{V}\wedge S\subseteq B\right)$$
8		eqid	$$⊢{+}_M={+}_M$$
9	1 8 2	cntzval	$$⊢S\subseteq B\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx{+}_{M}y=y{+}_{M}x\right\}$$
10	7 9	simpl2im	$$⊢x\in Z\left(S\right)\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx{+}_{M}y=y{+}_{M}x\right\}$$
11		ssrab2	$$⊢\left\{x\in B|\forall y\in Sx{+}_{M}y=y{+}_{M}x\right\}\subseteq B$$
12	10 11	eqsstrdi	$$⊢x\in Z\left(S\right)\to Z\left(S\right)\subseteq B$$
13	12	exlimiv	$$⊢\exists xx\in Z\left(S\right)\to Z\left(S\right)\subseteq B$$
14	6 13	sylbi	$$⊢Z\left(S\right)\ne \varnothing \to Z\left(S\right)\subseteq B$$
15	5 14	pm2.61ine	$$⊢Z\left(S\right)\subseteq B$$