Theorem ablcntzd

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

	Ref	Expression
Hypotheses	ablcntzd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	ablcntzd.a	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablcntzd.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	ablcntzd.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
Assertion	ablcntzd	$$⊢\phi \to T\subseteq Z\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		ablcntzd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
2		ablcntzd.a	$$⊢\phi \to G\in \mathrm{Abel}$$
3		ablcntzd.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
4		ablcntzd.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	5	subgss	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to T\subseteq {\mathrm{Base}}_G$$
7	3 6	syl	$$⊢\phi \to T\subseteq {\mathrm{Base}}_G$$
8		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
9	2 8	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
10	5	subgss	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to U\subseteq {\mathrm{Base}}_G$$
11	4 10	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_G$$
12	5 1	cntzcmn	$$⊢\left(G\in \mathrm{CMnd}\wedge U\subseteq {\mathrm{Base}}_G\right)\to Z\left(U\right)={\mathrm{Base}}_G$$
13	9 11 12	syl2anc	$$⊢\phi \to Z\left(U\right)={\mathrm{Base}}_G$$
14	7 13	sseqtrrd	$$⊢\phi \to T\subseteq Z\left(U\right)$$