lsmelvalmi

Description: Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmelvalm.m	$⊢ \underset{˙}{-} = -_{G}$
	lsmelvalm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmelvalm.t	$⊢ φ \to T \in SubGrp (G)$
	lsmelvalm.u	$⊢ φ \to U \in SubGrp (G)$
	lsmelvalmi.x	$⊢ φ \to X \in T$
	lsmelvalmi.y	$⊢ φ \to Y \in U$
Assertion	lsmelvalmi	$⊢ φ \to X \underset{˙}{-} Y \in (T \underset{˙}{\oplus} U)$

Step	Hyp	Ref	Expression
1		lsmelvalm.m	$⊢ \underset{˙}{-} = -_{G}$
2		lsmelvalm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		lsmelvalm.t	$⊢ φ \to T \in SubGrp (G)$
4		lsmelvalm.u	$⊢ φ \to U \in SubGrp (G)$
5		lsmelvalmi.x	$⊢ φ \to X \in T$
6		lsmelvalmi.y	$⊢ φ \to Y \in U$
7		eqidd	$⊢ φ \to X \underset{˙}{-} Y = X \underset{˙}{-} Y$
8		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$
9	5 6 7 8	syl3anc	$⊢ φ \to \exists x \in T \exists y \in U X \underset{˙}{-} Y = x \underset{˙}{-} y$
10	1 2 3 4	lsmelvalm	$⊢ φ \to (X \underset{˙}{-} Y \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists x \in T \exists y \in U X \underset{˙}{-} Y = x \underset{˙}{-} y)$
11	9 10	mpbird	$⊢ φ \to X \underset{˙}{-} Y \in (T \underset{˙}{\oplus} U)$

Metamath Proof Explorer