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

Metamath Proof Explorer

Theorem ablcntzd

Description: All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses ablcntzd.z 
|- Z = ( Cntz ` G )
ablcntzd.a 
|- ( ph -> G e. Abel )
ablcntzd.t 
|- ( ph -> T e. ( SubGrp ` G ) )
ablcntzd.u 
|- ( ph -> U e. ( SubGrp ` G ) )
Assertion ablcntzd 
|- ( ph -> T C_ ( Z ` U ) )

Proof

Step Hyp Ref Expression
1 ablcntzd.z 
 |-  Z = ( Cntz ` G )
2 ablcntzd.a 
 |-  ( ph -> G e. Abel )
3 ablcntzd.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
4 ablcntzd.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
7 3 6 syl 
 |-  ( ph -> T C_ ( Base ` G ) )
8 ablcmn 
 |-  ( G e. Abel -> G e. CMnd )
9 2 8 syl 
 |-  ( ph -> G e. CMnd )
10 5 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
11 4 10 syl 
 |-  ( ph -> U C_ ( Base ` G ) )
12 5 1 cntzcmn 
 |-  ( ( G e. CMnd /\ U C_ ( Base ` G ) ) -> ( Z ` U ) = ( Base ` G ) )
13 9 11 12 syl2anc 
 |-  ( ph -> ( Z ` U ) = ( Base ` G ) )
14 7 13 sseqtrrd 
 |-  ( ph -> T C_ ( Z ` U ) )