pj1fval

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	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))$

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		elex	$⊢ G \in V \to G \in V$
6	5	3ad2ant1	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to G \in V$
7		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
8	7 1	eqtr4di	$⊢ g = G \to {Base}_{g} = B$
9	8	pweqd	$⊢ g = G \to 𝒫 {Base}_{g} = 𝒫 B$
10		fveq2	$⊢ g = G \to LSSum (g) = LSSum (G)$
11	10 3	eqtr4di	$⊢ g = G \to LSSum (g) = \underset{˙}{\oplus}$
12	11	oveqd	$⊢ g = G \to t LSSum (g) u = t \underset{˙}{\oplus} u$
13		fveq2	$⊢ g = G \to +_{g} = +_{G}$
14	13 2	eqtr4di	$⊢ g = G \to +_{g} = \underset{˙}{+}$
15	14	oveqd	$⊢ g = G \to x +_{g} y = x \underset{˙}{+} y$
16	15	eqeq2d	$⊢ g = G \to (z = x +_{g} y \leftrightarrow z = x \underset{˙}{+} y)$
17	16	rexbidv	$⊢ g = G \to (\exists y \in u z = x +_{g} y \leftrightarrow \exists y \in u z = x \underset{˙}{+} y)$
18	17	riotabidv	$⊢ g = G \to (ι x \in t \| \exists y \in u z = x +_{g} y) = (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)$
19	12 18	mpteq12dv	$⊢ g = G \to (z \in (t LSSum (g) u) ⟼ (ι x \in t \| \exists y \in u z = x +_{g} y)) = (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y))$
20	9 9 19	mpoeq123dv	$⊢ g = G \to (t \in 𝒫 {Base}_{g}, u \in 𝒫 {Base}_{g} ⟼ (z \in (t LSSum (g) u) ⟼ (ι x \in t \| \exists y \in u z = x +_{g} y))) = (t \in 𝒫 B, u \in 𝒫 B ⟼ (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)))$
21		df-pj1	$⊢ {proj}_{1} = (g \in V ⟼ (t \in 𝒫 {Base}_{g}, u \in 𝒫 {Base}_{g} ⟼ (z \in (t LSSum (g) u) ⟼ (ι x \in t \| \exists y \in u z = x +_{g} y))))$
22	1	fvexi	$⊢ B \in V$
23	22	pwex	$⊢ 𝒫 B \in V$
24	23 23	mpoex	$⊢ (t \in 𝒫 B, u \in 𝒫 B ⟼ (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y))) \in V$
25	20 21 24	fvmpt	$⊢ G \in V \to {proj}_{1} (G) = (t \in 𝒫 B, u \in 𝒫 B ⟼ (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)))$
26	6 25	syl	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to {proj}_{1} (G) = (t \in 𝒫 B, u \in 𝒫 B ⟼ (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)))$
27	4 26	eqtrid	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to P = (t \in 𝒫 B, u \in 𝒫 B ⟼ (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)))$
28		oveq12	$⊢ (t = T \land u = U) \to t \underset{˙}{\oplus} u = T \underset{˙}{\oplus} U$
29	28	adantl	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to t \underset{˙}{\oplus} u = T \underset{˙}{\oplus} U$
30		simprl	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to t = T$
31		simprr	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to u = U$
32	31	rexeqdv	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to (\exists y \in u z = x \underset{˙}{+} y \leftrightarrow \exists y \in U z = x \underset{˙}{+} y)$
33	30 32	riotaeqbidv	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y) = (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y)$
34	29 33	mpteq12dv	$⊢ ((G \in V \land T \subseteq B \land U \subseteq B) \land (t = T \land u = U)) \to (z \in (t \underset{˙}{\oplus} u) ⟼ (ι x \in t \| \exists y \in u z = x \underset{˙}{+} y)) = (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y))$
35		simp2	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to T \subseteq B$
36	22	elpw2	$⊢ T \in 𝒫 B \leftrightarrow T \subseteq B$
37	35 36	sylibr	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to T \in 𝒫 B$
38		simp3	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to U \subseteq B$
39	22	elpw2	$⊢ U \in 𝒫 B \leftrightarrow U \subseteq B$
40	38 39	sylibr	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to U \in 𝒫 B$
41		ovex	$⊢ T \underset{˙}{\oplus} U \in V$
42	41	mptex	$⊢ (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y)) \in V$
43	42	a1i	$⊢ (G \in V \land T \subseteq B \land U \subseteq B) \to (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y)) \in V$
44	27 34 37 40 43	ovmpod	$⊢ (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))$

Metamath Proof Explorer

Theorem pj1fval

Proof