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 = Cntz (G)$
	Assertion	cntzidss	$⊢ (S \subseteq Z (S) \land T \subseteq S) \to T \subseteq Z (T)$

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

Metamath Proof Explorer