pj1ghm

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	pj1ghm	$⊢ φ \to T P U \in ((G ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom G)$

Proof

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		eqid	$⊢ {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} = {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12		ovex	$⊢ T \underset{˙}{\oplus} U \in V$
13		eqid	$⊢ G ↾_{𝑠} (T \underset{˙}{\oplus} U) = G ↾_{𝑠} (T \underset{˙}{\oplus} U)$
14	13 1	ressplusg	$⊢ T \underset{˙}{\oplus} U \in V \to \underset{˙}{+} = +_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
15	12 14	ax-mp	$⊢ \underset{˙}{+} = +_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
16	2 4	lsmsubg	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$
17	5 6 8 16	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U \in SubGrp (G)$
18	13	subggrp	$⊢ T \underset{˙}{\oplus} U \in SubGrp (G) \to G ↾_{𝑠} (T \underset{˙}{\oplus} U) \in Grp$
19	17 18	syl	$⊢ φ \to G ↾_{𝑠} (T \underset{˙}{\oplus} U) \in Grp$
20		subgrcl	$⊢ T \in SubGrp (G) \to G \in Grp$
21	5 20	syl	$⊢ φ \to G \in Grp$
22	1 2 3 4 5 6 7 8 9	pj1f	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
23	11	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
24	5 23	syl	$⊢ φ \to T \subseteq {Base}_{G}$
25	22 24	fssd	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ {Base}_{G}$
26	13	subgbas	$⊢ T \underset{˙}{\oplus} U \in SubGrp (G) \to T \underset{˙}{\oplus} U = {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
27	17 26	syl	$⊢ φ \to T \underset{˙}{\oplus} U = {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
28	27	feq2d	$⊢ φ \to ((T P U) : T \underset{˙}{\oplus} U ⟶ {Base}_{G} \leftrightarrow (T P U) : {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} ⟶ {Base}_{G})$
29	25 28	mpbid	$⊢ φ \to (T P U) : {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} ⟶ {Base}_{G}$
30	27	eleq2d	$⊢ φ \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow x \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))})$
31	27	eleq2d	$⊢ φ \to (y \in (T \underset{˙}{\oplus} U) \leftrightarrow y \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))})$
32	30 31	anbi12d	$⊢ φ \to ((x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \leftrightarrow (x \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} \land y \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))}))$
33	32	biimpar	$⊢ (φ \land (x \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} \land y \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))})) \to (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))$
34	1 2 3 4 5 6 7 8 9	pj1id	$⊢ (φ \land x \in (T \underset{˙}{\oplus} U)) \to x = (T P U) (x) \underset{˙}{+} (U P T) (x)$
35	34	adantrr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to x = (T P U) (x) \underset{˙}{+} (U P T) (x)$
36	1 2 3 4 5 6 7 8 9	pj1id	$⊢ (φ \land y \in (T \underset{˙}{\oplus} U)) \to y = (T P U) (y) \underset{˙}{+} (U P T) (y)$
37	36	adantrl	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to y = (T P U) (y) \underset{˙}{+} (U P T) (y)$
38	35 37	oveq12d	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to x \underset{˙}{+} y = ((T P U) (x) \underset{˙}{+} (U P T) (x)) \underset{˙}{+} ((T P U) (y) \underset{˙}{+} (U P T) (y))$
39	5	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to T \in SubGrp (G)$
40		grpmnd	$⊢ G \in Grp \to G \in Mnd$
41	39 20 40	3syl	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to G \in Mnd$
42	39 23	syl	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to T \subseteq {Base}_{G}$
43		simpl	$⊢ (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \to x \in (T \underset{˙}{\oplus} U)$
44		ffvelrn	$⊢ ((T P U) : T \underset{˙}{\oplus} U ⟶ T \land x \in (T \underset{˙}{\oplus} U)) \to (T P U) (x) \in T$
45	22 43 44	syl2an	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (x) \in T$
46	42 45	sseldd	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (x) \in {Base}_{G}$
47		simpr	$⊢ (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \to y \in (T \underset{˙}{\oplus} U)$
48		ffvelrn	$⊢ ((T P U) : T \underset{˙}{\oplus} U ⟶ T \land y \in (T \underset{˙}{\oplus} U)) \to (T P U) (y) \in T$
49	22 47 48	syl2an	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \in T$
50	42 49	sseldd	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \in {Base}_{G}$
51	6	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to U \in SubGrp (G)$
52	11	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
53	51 52	syl	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to U \subseteq {Base}_{G}$
54	1 2 3 4 5 6 7 8 9	pj2f	$⊢ φ \to (U P T) : T \underset{˙}{\oplus} U ⟶ U$
55		ffvelrn	$⊢ ((U P T) : T \underset{˙}{\oplus} U ⟶ U \land x \in (T \underset{˙}{\oplus} U)) \to (U P T) (x) \in U$
56	54 43 55	syl2an	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (x) \in U$
57	53 56	sseldd	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (x) \in {Base}_{G}$
58		ffvelrn	$⊢ ((U P T) : T \underset{˙}{\oplus} U ⟶ U \land y \in (T \underset{˙}{\oplus} U)) \to (U P T) (y) \in U$
59	54 47 58	syl2an	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (y) \in U$
60	53 59	sseldd	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (y) \in {Base}_{G}$
61	8	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to T \subseteq Z (U)$
62	61 49	sseldd	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \in Z (U)$
63	1 4	cntzi	$⊢ ((T P U) (y) \in Z (U) \land (U P T) (x) \in U) \to (T P U) (y) \underset{˙}{+} (U P T) (x) = (U P T) (x) \underset{˙}{+} (T P U) (y)$
64	62 56 63	syl2anc	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \underset{˙}{+} (U P T) (x) = (U P T) (x) \underset{˙}{+} (T P U) (y)$
65	11 1 41 46 50 57 60 64	mnd4g	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to ((T P U) (x) \underset{˙}{+} (T P U) (y)) \underset{˙}{+} ((U P T) (x) \underset{˙}{+} (U P T) (y)) = ((T P U) (x) \underset{˙}{+} (U P T) (x)) \underset{˙}{+} ((T P U) (y) \underset{˙}{+} (U P T) (y))$
66	38 65	eqtr4d	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to x \underset{˙}{+} y = ((T P U) (x) \underset{˙}{+} (T P U) (y)) \underset{˙}{+} ((U P T) (x) \underset{˙}{+} (U P T) (y))$
67	7	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to T \cap U = \{\underset{˙}{0}\}$
68	1	subgcl	$⊢ (T \underset{˙}{\oplus} U \in SubGrp (G) \land x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \to x \underset{˙}{+} y \in (T \underset{˙}{\oplus} U)$
69	68	3expb	$⊢ (T \underset{˙}{\oplus} U \in SubGrp (G) \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to x \underset{˙}{+} y \in (T \underset{˙}{\oplus} U)$
70	17 69	sylan	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to x \underset{˙}{+} y \in (T \underset{˙}{\oplus} U)$
71	1	subgcl	$⊢ (T \in SubGrp (G) \land (T P U) (x) \in T \land (T P U) (y) \in T) \to (T P U) (x) \underset{˙}{+} (T P U) (y) \in T$
72	39 45 49 71	syl3anc	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (x) \underset{˙}{+} (T P U) (y) \in T$
73	1	subgcl	$⊢ (U \in SubGrp (G) \land (U P T) (x) \in U \land (U P T) (y) \in U) \to (U P T) (x) \underset{˙}{+} (U P T) (y) \in U$
74	51 56 59 73	syl3anc	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (x) \underset{˙}{+} (U P T) (y) \in U$
75	1 2 3 4 39 51 67 61 9 70 72 74	pj1eq	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (x \underset{˙}{+} y = ((T P U) (x) \underset{˙}{+} (T P U) (y)) \underset{˙}{+} ((U P T) (x) \underset{˙}{+} (U P T) (y)) \leftrightarrow ((T P U) (x \underset{˙}{+} y) = (T P U) (x) \underset{˙}{+} (T P U) (y) \land (U P T) (x \underset{˙}{+} y) = (U P T) (x) \underset{˙}{+} (U P T) (y)))$
76	66 75	mpbid	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to ((T P U) (x \underset{˙}{+} y) = (T P U) (x) \underset{˙}{+} (T P U) (y) \land (U P T) (x \underset{˙}{+} y) = (U P T) (x) \underset{˙}{+} (U P T) (y))$
77	76	simpld	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (x \underset{˙}{+} y) = (T P U) (x) \underset{˙}{+} (T P U) (y)$
78	33 77	syldan	$⊢ (φ \land (x \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))} \land y \in {Base}_{(G ↾_{𝑠} (T \underset{˙}{\oplus} U))})) \to (T P U) (x \underset{˙}{+} y) = (T P U) (x) \underset{˙}{+} (T P U) (y)$
79	10 11 15 1 19 21 29 78	isghmd	$⊢ φ \to T P U \in ((G ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom G)$

Metamath Proof Explorer

Theorem pj1ghm

Proof