Theorem lsmless1

Description: Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypothesis	lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsmless1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑆 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		subgrcl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3	2	3ad2ant1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝐺 ∈ Grp )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	4	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
6	5	3ad2ant1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7	4	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
8	7	3ad2ant2	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9		simp3	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝑇 )
10	4 1	lsmless1x	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑆 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
11	3 6 8 9 10	syl31anc	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑆 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )