Metamath Proof Explorer

Theorem lsmssv

Description: Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lsmless2.v	$⊢ B = {Base}_{G}$
2		lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		eqid	$⊢ +_{G} = +_{G}$
4	1 3 2	lsmvalx	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to T \underset{˙}{\oplus} U = ran (x \in T, y \in U ⟼ x +_{G} y)$
5		simpl1	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (x \in T \land y \in U)) \to G \in Mnd$
6		simp2	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to T \subseteq B$
7	6	sselda	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land x \in T) \to x \in B$
8	7	adantrr	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (x \in T \land y \in U)) \to x \in B$
9		simp3	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to U \subseteq B$
10	9	sselda	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land y \in U) \to y \in B$
11	10	adantrl	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (x \in T \land y \in U)) \to y \in B$
12	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x +_{G} y \in B$
13	5 8 11 12	syl3anc	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (x \in T \land y \in U)) \to x +_{G} y \in B$
14	13	ralrimivva	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to \forall x \in T \forall y \in U x +_{G} y \in B$
15		eqid	$⊢ (x \in T, y \in U ⟼ x +_{G} y) = (x \in T, y \in U ⟼ x +_{G} y)$
16	15	fmpo	$⊢ \forall x \in T \forall y \in U x +_{G} y \in B \leftrightarrow (x \in T, y \in U ⟼ x +_{G} y) : T \times U ⟶ B$
17	14 16	sylib	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to (x \in T, y \in U ⟼ x +_{G} y) : T \times U ⟶ B$
18	17	frnd	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to ran (x \in T, y \in U ⟼ x +_{G} y) \subseteq B$
19	4 18	eqsstrd	$⊢ (G \in Mnd \land T \subseteq B \land U \subseteq B) \to T \underset{˙}{\oplus} U \subseteq B$