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	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion	cntzidss	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cntzmhm.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2		simpr	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑆 )
3		simpl	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	4 1	cntzssv	⊢ ( 𝑍 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 )
6	3 5	sstrdi	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
7	4 1	cntz2ss	⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) )
8	6 7	sylancom	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) )
9	3 8	sstrd	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) )
10	2 9	sstrd	⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑇 ) )