Theorem lsmless12

Description: Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		subgrcl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3	2	ad2antrr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝐺 ∈ Grp )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	4	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
6	5	ad2antrr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
7		simprr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑇 ⊆ 𝑈 )
8	4	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9	8	ad2antlr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
10	7 9	sstrd	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
11		simprl	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑅 ⊆ 𝑆 )
12	4 1	lsmless1x	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑅 ⊆ 𝑆 ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
13	3 6 10 11 12	syl31anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
14		simpll	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
15		simplr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
16	1	lsmless2	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑆 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )
17	14 15 7 16	syl3anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑆 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )
18	13 17	sstrd	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )