Metamath Proof Explorer

Theorem lsmless2x

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

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

Proof

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