This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )