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 𝑍 = ( 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 ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )