Metamath Proof Explorer

Theorem lsmless1x

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

		Ref	Expression
	Hypotheses	lsmless2.v	$⊢ B = {Base}_{G}$
		lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmless1x	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to R \underset{˙}{\oplus} U \subseteq T \underset{˙}{\oplus} U$

Proof

Step	Hyp	Ref	Expression
1		lsmless2.v	$⊢ B = {Base}_{G}$
2		lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		ssrexv	$⊢ R \subseteq T \to (\exists y \in R \exists z \in U x = y +_{G} z \to \exists y \in T \exists z \in U x = y +_{G} z)$
4	3	adantl	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to (\exists y \in R \exists z \in U x = y +_{G} z \to \exists y \in T \exists z \in U x = y +_{G} z)$
5		simpl1	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to G \in V$
6		simpr	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to R \subseteq T$
7		simpl2	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to T \subseteq B$
8	6 7	sstrd	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to R \subseteq B$
9		simpl3	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to U \subseteq B$
10		eqid	$⊢ +_{G} = +_{G}$
11	1 10 2	lsmelvalx	$⊢ (G \in V \land R \subseteq B \land U \subseteq B) \to (x \in (R \underset{˙}{\oplus} U) \leftrightarrow \exists y \in R \exists z \in U x = y +_{G} z)$
12	5 8 9 11	syl3anc	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to (x \in (R \underset{˙}{\oplus} U) \leftrightarrow \exists y \in R \exists z \in U x = y +_{G} z)$
13	1 10 2	lsmelvalx	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U x = y +_{G} z)$
14	13	adantr	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U x = y +_{G} z)$
15	4 12 14	3imtr4d	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to (x \in (R \underset{˙}{\oplus} U) \to x \in (T \underset{˙}{\oplus} U))$
16	15	ssrdv	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land R \subseteq T) \to R \underset{˙}{\oplus} U \subseteq T \underset{˙}{\oplus} U$