Theorem pj1ghm2

Description: The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

	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	pj1ghm2	$$⊢\phi \to TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}\left(G{\upharpoonright }_{𝑠}T\right)\right)$$

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	1 2 3 4 5 6 7 8 9	pj1ghm	$$⊢\phi \to TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}G\right)$$
11	1 2 3 4 5 6 7 8 9	pj1f	$$⊢\phi \to \left(TPU\right):T\underset{\dot{}}{\oplus }U⟶T$$
12	11	frnd	$$⊢\phi \to \mathrm{ran}\left(TPU\right)\subseteq T$$
13		eqid	$$⊢G{\upharpoonright }_{𝑠}T=G{\upharpoonright }_{𝑠}T$$
14	13	resghm2b	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge \mathrm{ran}\left(TPU\right)\subseteq T\right)\to \left(TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}G\right)\leftrightarrow TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}\left(G{\upharpoonright }_{𝑠}T\right)\right)\right)$$
15	5 12 14	syl2anc	$$⊢\phi \to \left(TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}G\right)\leftrightarrow TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}\left(G{\upharpoonright }_{𝑠}T\right)\right)\right)$$
16	10 15	mpbid	$$⊢\phi \to TPU\in \left(\left(G{\upharpoonright }_{𝑠}\left(T\underset{\dot{}}{\oplus }U\right)\right)\mathrm{GrpHom}\left(G{\upharpoonright }_{𝑠}T\right)\right)$$