Step |
Hyp |
Ref |
Expression |
1 |
|
lsmub1.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
2 |
|
ssid |
⊢ 𝑈 ⊆ 𝑈 |
3 |
1
|
lsmlub |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑈 ) ) |
4 |
3
|
3anidm23 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑈 ) ) |
5 |
4
|
biimpd |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑈 ) ) |
6 |
2 5
|
mpan2i |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑈 ) ) |
7 |
6
|
3impia |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑈 ) |
8 |
1
|
lsmub2 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
9 |
8
|
3adant3 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
10 |
7 9
|
eqssd |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) |