Theorem pj1f

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

	Ref	Expression
Hypotheses	pj1eu.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	pj1eu.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	pj1eu.o	$$⊢\underset{\dot{}}{0}=0_G$$
	pj1eu.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	pj1eu.2	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	pj1eu.3	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	pj1eu.4	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
	pj1eu.5	$$⊢\phi \to T\subseteq Z\left(U\right)$$
	pj1f.p	$$⊢P={proj}_1\left(G\right)$$
Assertion	pj1f	$$⊢\phi \to \left(TPU\right):T\underset{\dot{}}{\oplus }U⟶T$$

Proof

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