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