Metamath Proof Explorer

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	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmless12	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to R \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} U$

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
3	2	ad2antrr	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to G \in Grp$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	4	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
6	5	ad2antrr	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to S \subseteq {Base}_{G}$
7		simprr	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to T \subseteq U$
8	4	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
9	8	ad2antlr	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to U \subseteq {Base}_{G}$
10	7 9	sstrd	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to T \subseteq {Base}_{G}$
11		simprl	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to R \subseteq S$
12	4 1	lsmless1x	$⊢ ((G \in Grp \land S \subseteq {Base}_{G} \land T \subseteq {Base}_{G}) \land R \subseteq S) \to R \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} T$
13	3 6 10 11 12	syl31anc	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to R \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} T$
14		simpll	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to S \in SubGrp (G)$
15		simplr	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to U \in SubGrp (G)$
16	1	lsmless2	$⊢ (S \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq U) \to S \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} U$
17	14 15 7 16	syl3anc	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to S \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} U$
18	13 17	sstrd	$⊢ ((S \in SubGrp (G) \land U \in SubGrp (G)) \land (R \subseteq S \land T \subseteq U)) \to R \underset{˙}{\oplus} T \subseteq S \underset{˙}{\oplus} U$