Theorem lsmub1

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	lsmub1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3	2	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
4		subgsubm	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) )
5	2 1	lsmub1x	⊢ ( ( 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
6	3 4 5	syl2an	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )