Metamath Proof Explorer

Theorem pj1val

Description: The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Hypotheses	pj1fval.v	$⊢ B = {Base}_{G}$
		pj1fval.a	$⊢ \underset{˙}{+} = +_{G}$
		pj1fval.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
		pj1fval.p	$⊢ P = {proj}_{1} (G)$
	Assertion	pj1val	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \to (T P U) (X) = (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y)$

Proof

Step	Hyp	Ref	Expression
1		pj1fval.v	$⊢ B = {Base}_{G}$
2		pj1fval.a	$⊢ \underset{˙}{+} = +_{G}$
3		pj1fval.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
4		pj1fval.p	$⊢ P = {proj}_{1} (G)$
5	1 2 3 4	pj1fval	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to T P U = (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y))$
6	5	adantr	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \to T P U = (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y))$
7		simpr	$⊢ (((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \land z = X) \to z = X$
8	7	eqeq1d	$⊢ (((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \land z = X) \to (z = x \underset{˙}{+} y \leftrightarrow X = x \underset{˙}{+} y)$
9	8	rexbidv	$⊢ (((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \land z = X) \to (\exists y \in U z = x \underset{˙}{+} y \leftrightarrow \exists y \in U X = x \underset{˙}{+} y)$
10	9	riotabidv	$⊢ (((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \land z = X) \to (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y) = (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y)$
11		simpr	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \to X \in (T \underset{˙}{\oplus} U)$
12		riotaex	$⊢ (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y) \in V$
13	12	a1i	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \to (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y) \in V$
14	6 10 11 13	fvmptd	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land X \in (T \underset{˙}{\oplus} U)) \to (T P U) (X) = (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y)$