pj1f

Description: The left projection function maps a direct subspace sum onto the left factor. (Contributed by Mario Carneiro, 15-Oct-2015)

Step	Hyp	Ref	Expression
1		pj1eu.a	$⊢ \underset{˙}{+} = +_{G}$
2		pj1eu.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		pj1eu.o	$⊢ \underset{˙}{0} = 0_{G}$
4		pj1eu.z	$⊢ Z = Cntz (G)$
5		pj1eu.2	$⊢ φ \to T \in SubGrp (G)$
6		pj1eu.3	$⊢ φ \to U \in SubGrp (G)$
7		pj1eu.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
8		pj1eu.5	$⊢ φ \to T \subseteq Z (U)$
9		pj1f.p	$⊢ P = {proj}_{1} (G)$
10		subgrcl	$⊢ T \in SubGrp (G) \to G \in Grp$
11	5 10	syl	$⊢ φ \to G \in Grp$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13	12	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
14	5 13	syl	$⊢ φ \to T \subseteq {Base}_{G}$
15	12	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
16	6 15	syl	$⊢ φ \to U \subseteq {Base}_{G}$
17	12 1 2 9	pj1fval	$⊢ (G \in Grp \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to T P U = (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y))$
18	11 14 16 17	syl3anc	$⊢ φ \to T P U = (z \in (T \underset{˙}{\oplus} U) ⟼ (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y))$
19	1 2 3 4 5 6 7 8	pj1eu	$⊢ (φ \land z \in (T \underset{˙}{\oplus} U)) \to \exists! x \in T \exists y \in U z = x \underset{˙}{+} y$
20		riotacl	$⊢ \exists! x \in T \exists y \in U z = x \underset{˙}{+} y \to (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y) \in T$
21	19 20	syl	$⊢ (φ \land z \in (T \underset{˙}{\oplus} U)) \to (ι x \in T \| \exists y \in U z = x \underset{˙}{+} y) \in T$
22	18 21	fmpt3d	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$

Metamath Proof Explorer