Step |
Hyp |
Ref |
Expression |
1 |
|
cntrcmnd.z |
⊢ 𝑍 = ( 𝑀 ↾s ( Cntr ‘ 𝑀 ) ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
3 |
|
eqid |
⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 ) |
4 |
2 3
|
cntrval |
⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 ) |
5 |
|
ssid |
⊢ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) |
6 |
2 3
|
cntzsubg |
⊢ ( ( 𝑀 ∈ Grp ∧ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) ) → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) ) |
7 |
5 6
|
mpan2 |
⊢ ( 𝑀 ∈ Grp → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) ) |
8 |
4 7
|
eqeltrrid |
⊢ ( 𝑀 ∈ Grp → ( Cntr ‘ 𝑀 ) ∈ ( SubGrp ‘ 𝑀 ) ) |
9 |
1
|
subggrp |
⊢ ( ( Cntr ‘ 𝑀 ) ∈ ( SubGrp ‘ 𝑀 ) → 𝑍 ∈ Grp ) |
10 |
8 9
|
syl |
⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ Grp ) |
11 |
|
grpmnd |
⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd ) |
12 |
1
|
cntrcmnd |
⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ CMnd ) |
13 |
11 12
|
syl |
⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ CMnd ) |
14 |
|
isabl |
⊢ ( 𝑍 ∈ Abel ↔ ( 𝑍 ∈ Grp ∧ 𝑍 ∈ CMnd ) ) |
15 |
10 13 14
|
sylanbrc |
⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ Abel ) |