Step |
Hyp |
Ref |
Expression |
1 |
|
ablcntzd.z |
|- Z = ( Cntz ` G ) |
2 |
|
ablcntzd.a |
|- ( ph -> G e. Abel ) |
3 |
|
ablcntzd.t |
|- ( ph -> T e. ( SubGrp ` G ) ) |
4 |
|
ablcntzd.u |
|- ( ph -> U e. ( SubGrp ` G ) ) |
5 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
6 |
5
|
subgss |
|- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) ) |
7 |
3 6
|
syl |
|- ( ph -> T C_ ( Base ` G ) ) |
8 |
|
ablcmn |
|- ( G e. Abel -> G e. CMnd ) |
9 |
2 8
|
syl |
|- ( ph -> G e. CMnd ) |
10 |
5
|
subgss |
|- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) ) |
11 |
4 10
|
syl |
|- ( ph -> U C_ ( Base ` G ) ) |
12 |
5 1
|
cntzcmn |
|- ( ( G e. CMnd /\ U C_ ( Base ` G ) ) -> ( Z ` U ) = ( Base ` G ) ) |
13 |
9 11 12
|
syl2anc |
|- ( ph -> ( Z ` U ) = ( Base ` G ) ) |
14 |
7 13
|
sseqtrrd |
|- ( ph -> T C_ ( Z ` U ) ) |