Step |
Hyp |
Ref |
Expression |
1 |
|
lsmcom.s |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
2 |
|
simp2 |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) |
3 |
|
simp3 |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) |
4 |
|
eqid |
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 ) |
5 |
|
simp1 |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Abel ) |
6 |
4 5 2 3
|
ablcntzd |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝑈 ) ) |
7 |
1 4
|
lsmsubg |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
8 |
2 3 6 7
|
syl3anc |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ) |