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