Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lsmub1.p | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | |
Assertion | lsmub2 | ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmub1.p | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | |
2 | subgsubm | ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ) | |
3 | eqid | ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) | |
4 | 3 | subgss | ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
5 | 3 1 | lsmub2x | ⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
6 | 2 4 5 | syl2an | ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |