Theorem ablcntzd

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

	Ref	Expression
Hypotheses	ablcntzd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	ablcntzd.a	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablcntzd.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	ablcntzd.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion	ablcntzd	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ablcntzd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2		ablcntzd.a	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3		ablcntzd.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4		ablcntzd.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	5	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7	3 6	syl	⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
8		ablcmn	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
9	2 8	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
10	5	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
11	4 10	syl	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
12	5 1	cntzcmn	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍 ‘ 𝑈 ) = ( Base ‘ 𝐺 ) )
13	9 11 12	syl2anc	⊢ ( 𝜑 → ( 𝑍 ‘ 𝑈 ) = ( Base ‘ 𝐺 ) )
14	7 13	sseqtrrd	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )