This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmelvalx

Description: Subspace sum membership (for a group or vector space). Extended domain version of lsmelval . (Contributed by NM, 28-Jan-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	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 \underset{˙}{+} z)$

Proof

Step	Hyp	Ref	Expression
1		lsmfval.v	$⊢ B = {Base}_{G}$
2		lsmfval.a	$⊢ \underset{˙}{+} = +_{G}$
3		lsmfval.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
4	1 2 3	lsmvalx	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to T \underset{˙}{\oplus} U = ran (y \in T, z \in U ⟼ y \underset{˙}{+} z)$
5	4	eleq2d	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow X \in ran (y \in T, z \in U ⟼ y \underset{˙}{+} z))$
6		eqid	$⊢ (y \in T, z \in U ⟼ y \underset{˙}{+} z) = (y \in T, z \in U ⟼ y \underset{˙}{+} z)$
7		ovex	$⊢ y \underset{˙}{+} z \in V$
8	6 7	elrnmpo	$⊢ X \in ran (y \in T, z \in U ⟼ y \underset{˙}{+} z) \leftrightarrow \exists y \in T \exists z \in U X = y \underset{˙}{+} z$
9	5 8	bitrdi	$⊢ (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 \underset{˙}{+} z)$