This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)
|
|
Ref |
Expression |
|
Hypothesis |
lsmub1.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
|
Assertion |
lsmunss |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lsmub1.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
| 2 |
1
|
lsmub1 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
| 3 |
1
|
lsmub2 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
| 4 |
2 3
|
unssd |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) |