Metamath Proof Explorer


Theorem lsmub2

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 ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 𝑈 ) )

Proof

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 ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 𝑈 ) )