ablcntzd

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

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

Metamath Proof Explorer