Theorem cntz2ss

Description: Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	cntzrec.b	$$⊢B={\mathrm{Base}}_M$$
	cntzrec.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntz2ss	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to Z\left(S\right)\subseteq Z\left(T\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	3 2	cntzi	$$⊢\left(x\in Z\left(S\right)\wedge y\in S\right)\to x{+}_{M}y=y{+}_{M}x$$
5	4	ralrimiva	$$⊢x\in Z\left(S\right)\to \forall y\in Sx{+}_{M}y=y{+}_{M}x$$
6		ssralv	$$⊢T\subseteq S\to \left(\forall y\in Sx{+}_{M}y=y{+}_{M}x\to \forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
7	6	adantl	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to \left(\forall y\in Sx{+}_{M}y=y{+}_{M}x\to \forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
8	5 7	syl5	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to \left(x\in Z\left(S\right)\to \forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
9	8	ralrimiv	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to \forall x\in Z\left(S\right)\forall y\in Tx{+}_{M}y=y{+}_{M}x$$
10	1 2	cntzssv	$$⊢Z\left(S\right)\subseteq B$$
11		sstr	$$⊢\left(T\subseteq S\wedge S\subseteq B\right)\to T\subseteq B$$
12	11	ancoms	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to T\subseteq B$$
13	1 3 2	sscntz	$$⊢\left(Z\left(S\right)\subseteq B\wedge T\subseteq B\right)\to \left(Z\left(S\right)\subseteq Z\left(T\right)\leftrightarrow \forall x\in Z\left(S\right)\forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
14	10 12 13	sylancr	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to \left(Z\left(S\right)\subseteq Z\left(T\right)\leftrightarrow \forall x\in Z\left(S\right)\forall y\in Tx{+}_{M}y=y{+}_{M}x\right)$$
15	9 14	mpbird	$$⊢\left(S\subseteq B\wedge T\subseteq S\right)\to Z\left(S\right)\subseteq Z\left(T\right)$$