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