Theorem cntzidss

Description: If the elements of S commute, the elements of a subset T also commute. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypothesis	cntzmhm.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
Assertion	cntzidss	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to T\subseteq Z\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzmhm.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
2		simpr	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to T\subseteq S$$
3		simpl	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to S\subseteq Z\left(S\right)$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	4 1	cntzssv	$$⊢Z\left(S\right)\subseteq {\mathrm{Base}}_G$$
6	3 5	sstrdi	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to S\subseteq {\mathrm{Base}}_G$$
7	4 1	cntz2ss	$$⊢\left(S\subseteq {\mathrm{Base}}_G\wedge T\subseteq S\right)\to Z\left(S\right)\subseteq Z\left(T\right)$$
8	6 7	sylancom	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to Z\left(S\right)\subseteq Z\left(T\right)$$
9	3 8	sstrd	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to S\subseteq Z\left(T\right)$$
10	2 9	sstrd	$$⊢\left(S\subseteq Z\left(S\right)\wedge T\subseteq S\right)\to T\subseteq Z\left(T\right)$$