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 = ( Cntz ` G )
Assertion	cntzidss	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> T C_ ( Z ` T ) )

Proof

Step	Hyp	Ref	Expression
1		cntzmhm.z	|- Z = ( Cntz ` G )
2		simpr	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> T C_ S )
3		simpl	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> S C_ ( Z ` S ) )
4		eqid	|- ( Base ` G ) = ( Base ` G )
5	4 1	cntzssv	|- ( Z ` S ) C_ ( Base ` G )
6	3 5	sstrdi	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> S C_ ( Base ` G ) )
7	4 1	cntz2ss	|- ( ( S C_ ( Base ` G ) /\ T C_ S ) -> ( Z ` S ) C_ ( Z ` T ) )
8	6 7	sylancom	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> ( Z ` S ) C_ ( Z ` T ) )
9	3 8	sstrd	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> S C_ ( Z ` T ) )
10	2 9	sstrd	|- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> T C_ ( Z ` T ) )