pj1ghm2

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

	Ref	Expression
Hypotheses	pj1eu.a	$⊢ \underset{˙}{+} = +_{G}$
	pj1eu.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	pj1eu.o	$⊢ \underset{˙}{0} = 0_{G}$
	pj1eu.z	$⊢ Z = Cntz (G)$
	pj1eu.2	$⊢ φ \to T \in SubGrp (G)$
	pj1eu.3	$⊢ φ \to U \in SubGrp (G)$
	pj1eu.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	pj1eu.5	$⊢ φ \to T \subseteq Z (U)$
	pj1f.p	$⊢ P = {proj}_{1} (G)$
Assertion	pj1ghm2	$⊢ φ \to T P U \in ((G ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom (G ↾_{𝑠} T))$

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

Metamath Proof Explorer