This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )