ghmquskerlem3

Description: The mapping H induced by a surjective group homomorphism F from the quotient group Q over F 's kernel K is a group isomorphism. In this case, one says that F factors through Q , which is also called the factor group. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
	ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
	ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
	ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
Assertion	ghmquskerlem3	$⊢ φ \to J \in (Q GrpHom H)$

Proof

Step	Hyp	Ref	Expression
1		ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
3		ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
7		eqid	$⊢ {Base}_{H} = {Base}_{H}$
8		eqid	$⊢ +_{Q} = +_{Q}$
9		eqid	$⊢ +_{H} = +_{H}$
10	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
11	2 10	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
12	3 11	eqeltrid	$⊢ φ \to K \in NrmSGrp (G)$
13	4	qusgrp	$⊢ K \in NrmSGrp (G) \to Q \in Grp$
14	12 13	syl	$⊢ φ \to Q \in Grp$
15		ghmrn	$⊢ F \in (G GrpHom H) \to ran F \in SubGrp (H)$
16		subgrcl	$⊢ ran F \in SubGrp (H) \to H \in Grp$
17	2 15 16	3syl	$⊢ φ \to H \in Grp$
18	2	adantr	$⊢ (φ \land q \in {Base}_{Q}) \to F \in (G GrpHom H)$
19	18	imaexd	$⊢ (φ \land q \in {Base}_{Q}) \to F [q] \in V$
20	19	uniexd	$⊢ (φ \land q \in {Base}_{Q}) \to ⋃ F [q] \in V$
21	5	a1i	$⊢ φ \to J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
22		simpr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r) = F (x)$
23		eqid	$⊢ {Base}_{G} = {Base}_{G}$
24	23 7	ghmf	$⊢ F \in (G GrpHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
25	2 24	syl	$⊢ φ \to F : {Base}_{G} ⟶ {Base}_{H}$
26	25	frnd	$⊢ φ \to ran F \subseteq {Base}_{H}$
27	26	ad3antrrr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to ran F \subseteq {Base}_{H}$
28	25	ffnd	$⊢ φ \to F Fn {Base}_{G}$
29	28	ad3antrrr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F Fn {Base}_{G}$
30	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
31		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
32		ovexd	$⊢ φ \to G ~_{QG} K \in V$
33		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
34	2 33	syl	$⊢ φ \to G \in Grp$
35	30 31 32 34	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
36		nsgsubg	$⊢ K \in NrmSGrp (G) \to K \in SubGrp (G)$
37		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
38	23 37	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
39	12 36 38	3syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
40	39	qsss	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) \subseteq 𝒫 {Base}_{G}$
41	35 40	eqsstrrd	$⊢ φ \to {Base}_{Q} \subseteq 𝒫 {Base}_{G}$
42	41	sselda	$⊢ (φ \land r \in {Base}_{Q}) \to r \in 𝒫 {Base}_{G}$
43	42	elpwid	$⊢ (φ \land r \in {Base}_{Q}) \to r \subseteq {Base}_{G}$
44	43	sselda	$⊢ ((φ \land r \in {Base}_{Q}) \land x \in r) \to x \in {Base}_{G}$
45	44	adantr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to x \in {Base}_{G}$
46	29 45	fnfvelrnd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F (x) \in ran F$
47	27 46	sseldd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F (x) \in {Base}_{H}$
48	22 47	eqeltrd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r) \in {Base}_{H}$
49	2	adantr	$⊢ (φ \land r \in {Base}_{Q}) \to F \in (G GrpHom H)$
50		simpr	$⊢ (φ \land r \in {Base}_{Q}) \to r \in {Base}_{Q}$
51	1 49 3 4 5 50	ghmquskerlem2	$⊢ (φ \land r \in {Base}_{Q}) \to \exists x \in r J (r) = F (x)$
52	48 51	r19.29a	$⊢ (φ \land r \in {Base}_{Q}) \to J (r) \in {Base}_{H}$
53	20 21 52	fmpt2d	$⊢ φ \to J : {Base}_{Q} ⟶ {Base}_{H}$
54	39	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to (G ~_{QG} K) Er {Base}_{G}$
55	50	ad5antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \in {Base}_{Q}$
56	35	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
57	55 56	eleqtrrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \in ({Base}_{G} / (G ~_{QG} K))$
58		simp-4r	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x \in r$
59		qsel	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land r \in ({Base}_{G} / (G ~_{QG} K)) \land x \in r) \to r = [x] (G ~_{QG} K)$
60	54 57 58 59	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r = [x] (G ~_{QG} K)$
61		simp-5r	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \in {Base}_{Q}$
62	61 56	eleqtrrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \in ({Base}_{G} / (G ~_{QG} K))$
63		simplr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to y \in s$
64		qsel	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land s \in ({Base}_{G} / (G ~_{QG} K)) \land y \in s) \to s = [y] (G ~_{QG} K)$
65	54 62 63 64	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s = [y] (G ~_{QG} K)$
66	60 65	oveq12d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r +_{Q} s = [x] (G ~_{QG} K) +_{Q} [y] (G ~_{QG} K)$
67	12	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to K \in NrmSGrp (G)$
68	43	ad5antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \subseteq {Base}_{G}$
69	68 58	sseldd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x \in {Base}_{G}$
70	41	sselda	$⊢ (φ \land s \in {Base}_{Q}) \to s \in 𝒫 {Base}_{G}$
71	70	elpwid	$⊢ (φ \land s \in {Base}_{Q}) \to s \subseteq {Base}_{G}$
72	71	adantlr	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to s \subseteq {Base}_{G}$
73	72	ad4antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \subseteq {Base}_{G}$
74	73 63	sseldd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to y \in {Base}_{G}$
75		eqid	$⊢ +_{G} = +_{G}$
76	4 23 75 8	qusadd	$⊢ (K \in NrmSGrp (G) \land x \in {Base}_{G} \land y \in {Base}_{G}) \to [x] (G ~_{QG} K) +_{Q} [y] (G ~_{QG} K) = [(x +_{G} y)] (G ~_{QG} K)$
77	67 69 74 76	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to [x] (G ~_{QG} K) +_{Q} [y] (G ~_{QG} K) = [(x +_{G} y)] (G ~_{QG} K)$
78	66 77	eqtrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r +_{Q} s = [(x +_{G} y)] (G ~_{QG} K)$
79	78	fveq2d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r +_{Q} s) = J ([(x +_{G} y)] (G ~_{QG} K))$
80	2	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to F \in (G GrpHom H)$
81	80 33	syl	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to G \in Grp$
82	23 75 81 69 74	grpcld	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x +_{G} y \in {Base}_{G}$
83	1 80 3 4 5 82	ghmquskerlem1	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J ([(x +_{G} y)] (G ~_{QG} K)) = F (x +_{G} y)$
84	23 75 9	ghmlin	$⊢ (F \in (G GrpHom H) \land x \in {Base}_{G} \land y \in {Base}_{G}) \to F (x +_{G} y) = F (x) +_{H} F (y)$
85	80 69 74 84	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to F (x +_{G} y) = F (x) +_{H} F (y)$
86	79 83 85	3eqtrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r +_{Q} s) = F (x) +_{H} F (y)$
87		simpllr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r) = F (x)$
88		simpr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (s) = F (y)$
89	87 88	oveq12d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r) +_{H} J (s) = F (x) +_{H} F (y)$
90	86 89	eqtr4d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r +_{Q} s) = J (r) +_{H} J (s)$
91	2	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F \in (G GrpHom H)$
92		simpllr	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to s \in {Base}_{Q}$
93	1 91 3 4 5 92	ghmquskerlem2	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to \exists y \in s J (s) = F (y)$
94	90 93	r19.29a	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r +_{Q} s) = J (r) +_{H} J (s)$
95	51	adantr	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to \exists x \in r J (r) = F (x)$
96	94 95	r19.29a	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to J (r +_{Q} s) = J (r) +_{H} J (s)$
97	96	anasss	$⊢ (φ \land (r \in {Base}_{Q} \land s \in {Base}_{Q})) \to J (r +_{Q} s) = J (r) +_{H} J (s)$
98	6 7 8 9 14 17 53 97	isghmd	$⊢ φ \to J \in (Q GrpHom H)$

Metamath Proof Explorer

Theorem ghmquskerlem3

Proof