lsmelvalix

Description: Subspace sum membership (for a group or vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmfval.v	$⊢ B = {Base}_{G}$
	lsmfval.a	$⊢ \underset{˙}{+} = +_{G}$
	lsmfval.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	lsmelvalix	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (X \in T \land Y \in U)) \to X \underset{˙}{+} Y \in (T \underset{˙}{\oplus} U)$

Step	Hyp	Ref	Expression
1		lsmfval.v	$⊢ B = {Base}_{G}$
2		lsmfval.a	$⊢ \underset{˙}{+} = +_{G}$
3		lsmfval.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
4		eqid	$⊢ X \underset{˙}{+} Y = X \underset{˙}{+} Y$
5		rspceov	$⊢ (X \in T \land Y \in U \land X \underset{˙}{+} Y = X \underset{˙}{+} Y) \to \exists x \in T \exists y \in U X \underset{˙}{+} Y = x \underset{˙}{+} y$
6	4 5	mp3an3	$⊢ (X \in T \land Y \in U) \to \exists x \in T \exists y \in U X \underset{˙}{+} Y = x \underset{˙}{+} y$
7	1 2 3	lsmelvalx	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to (X \underset{˙}{+} Y \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists x \in T \exists y \in U X \underset{˙}{+} Y = x \underset{˙}{+} y)$
8	7	biimpar	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land \exists x \in T \exists y \in U X \underset{˙}{+} Y = x \underset{˙}{+} y) \to X \underset{˙}{+} Y \in (T \underset{˙}{\oplus} U)$
9	6 8	sylan2	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (X \in T \land Y \in U)) \to X \underset{˙}{+} Y \in (T \underset{˙}{\oplus} U)$

Metamath Proof Explorer