ghmqusnsg

Description: The mapping H induced by a surjective group homomorphism F from the quotient group Q over a normal subgroup N of 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, 13-May-2025)

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

Proof

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

Metamath Proof Explorer

Theorem ghmqusnsg

Proof