ghmqusker

Description: A surjective group homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 15-Feb-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])$
	ghmqusker.s	$⊢ φ \to ran F = {Base}_{H}$
Assertion	ghmqusker	$⊢ φ \to J \in (Q GrpIso 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		ghmqusker.s	$⊢ φ \to ran F = {Base}_{H}$
7	1 2 3 4 5	ghmquskerlem3	$⊢ φ \to J \in (Q GrpHom H)$
8		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
9	2 8	syl	$⊢ φ \to G \in Grp$
10	9	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to G \in Grp$
11	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
12	2 11	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
13	3 12	eqeltrid	$⊢ φ \to K \in NrmSGrp (G)$
14		nsgsubg	$⊢ K \in NrmSGrp (G) \to K \in SubGrp (G)$
15	13 14	syl	$⊢ φ \to K \in SubGrp (G)$
16	15	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to K \in SubGrp (G)$
17		eqid	$⊢ {Base}_{G} = {Base}_{G}$
18		eqid	$⊢ {Base}_{H} = {Base}_{H}$
19	17 18	ghmf	$⊢ F \in (G GrpHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
20	2 19	syl	$⊢ φ \to F : {Base}_{G} ⟶ {Base}_{H}$
21	20	ffnd	$⊢ φ \to F Fn {Base}_{G}$
22	21	ad3antrrr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F Fn {Base}_{G}$
23	22	adantr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to F Fn {Base}_{G}$
24	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
25		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
26		ovexd	$⊢ φ \to G ~_{QG} K \in V$
27	24 25 26 9	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
28		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
29	17 28	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
30	13 14 29	3syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
31	30	qsss	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) \subseteq 𝒫 {Base}_{G}$
32	27 31	eqsstrrd	$⊢ φ \to {Base}_{Q} \subseteq 𝒫 {Base}_{G}$
33	32	sselda	$⊢ (φ \land r \in {Base}_{Q}) \to r \in 𝒫 {Base}_{G}$
34	33	elpwid	$⊢ (φ \land r \in {Base}_{Q}) \to r \subseteq {Base}_{G}$
35	34	sselda	$⊢ ((φ \land r \in {Base}_{Q}) \land x \in r) \to x \in {Base}_{G}$
36	35	adantr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to x \in {Base}_{G}$
37	36	adantr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to x \in {Base}_{G}$
38		simpr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r) = F (x)$
39	38	eqeq1d	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to (J (r) = \underset{˙}{0} \leftrightarrow F (x) = \underset{˙}{0})$
40	39	biimpa	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to F (x) = \underset{˙}{0}$
41		fniniseg	$⊢ F Fn {Base}_{G} \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in {Base}_{G} \land F (x) = \underset{˙}{0}))$
42	41	biimpar	$⊢ (F Fn {Base}_{G} \land (x \in {Base}_{G} \land F (x) = \underset{˙}{0})) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
43	23 37 40 42	syl12anc	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
44	43 3	eleqtrrdi	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to x \in K$
45	28	eqg0el	$⊢ (G \in Grp \land K \in SubGrp (G)) \to ([x] (G ~_{QG} K) = K \leftrightarrow x \in K)$
46	45	biimpar	$⊢ ((G \in Grp \land K \in SubGrp (G)) \land x \in K) \to [x] (G ~_{QG} K) = K$
47	10 16 44 46	syl21anc	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to [x] (G ~_{QG} K) = K$
48	30	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to (G ~_{QG} K) Er {Base}_{G}$
49		simpr	$⊢ (φ \land r \in {Base}_{Q}) \to r \in {Base}_{Q}$
50	27	adantr	$⊢ (φ \land r \in {Base}_{Q}) \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
51	49 50	eleqtrrd	$⊢ (φ \land r \in {Base}_{Q}) \to r \in ({Base}_{G} / (G ~_{QG} K))$
52	51	ad3antrrr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to r \in ({Base}_{G} / (G ~_{QG} K))$
53		simpllr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to x \in r$
54		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)$
55	48 52 53 54	syl3anc	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to r = [x] (G ~_{QG} K)$
56		eqid	$⊢ 0_{G} = 0_{G}$
57	17 28 56	eqgid	$⊢ K \in SubGrp (G) \to [0_{G}] (G ~_{QG} K) = K$
58	15 57	syl	$⊢ φ \to [0_{G}] (G ~_{QG} K) = K$
59	58	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to [0_{G}] (G ~_{QG} K) = K$
60	47 55 59	3eqtr4d	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to r = [0_{G}] (G ~_{QG} K)$
61	4 56	qus0	$⊢ K \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} K) = 0_{Q}$
62	13 61	syl	$⊢ φ \to [0_{G}] (G ~_{QG} K) = 0_{Q}$
63	62	ad3antrrr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to [0_{G}] (G ~_{QG} K) = 0_{Q}$
64	63	adantr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to [0_{G}] (G ~_{QG} K) = 0_{Q}$
65	60 64	eqtrd	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land J (r) = \underset{˙}{0}) \to r = 0_{Q}$
66	63	eqeq2d	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to (r = [0_{G}] (G ~_{QG} K) \leftrightarrow r = 0_{Q})$
67	66	biimpar	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to r = [0_{G}] (G ~_{QG} K)$
68	67	fveq2d	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to J (r) = J ([0_{G}] (G ~_{QG} K))$
69	2	adantr	$⊢ (φ \land r \in {Base}_{Q}) \to F \in (G GrpHom H)$
70	69	ad3antrrr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to F \in (G GrpHom H)$
71	17 56	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
72	9 71	syl	$⊢ φ \to 0_{G} \in {Base}_{G}$
73	72	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to 0_{G} \in {Base}_{G}$
74	1 70 3 4 5 73	ghmquskerlem1	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to J ([0_{G}] (G ~_{QG} K)) = F (0_{G})$
75	56 1	ghmid	$⊢ F \in (G GrpHom H) \to F (0_{G}) = \underset{˙}{0}$
76	2 75	syl	$⊢ φ \to F (0_{G}) = \underset{˙}{0}$
77	76	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to F (0_{G}) = \underset{˙}{0}$
78	68 74 77	3eqtrd	$⊢ ((((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land r = 0_{Q}) \to J (r) = \underset{˙}{0}$
79	65 78	impbida	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to (J (r) = \underset{˙}{0} \leftrightarrow r = 0_{Q})$
80	1 69 3 4 5 49	ghmquskerlem2	$⊢ (φ \land r \in {Base}_{Q}) \to \exists x \in r J (r) = F (x)$
81	79 80	r19.29a	$⊢ (φ \land r \in {Base}_{Q}) \to (J (r) = \underset{˙}{0} \leftrightarrow r = 0_{Q})$
82	81	pm5.32da	$⊢ φ \to ((r \in {Base}_{Q} \land J (r) = \underset{˙}{0}) \leftrightarrow (r \in {Base}_{Q} \land r = 0_{Q}))$
83		simpr	$⊢ (φ \land r = 0_{Q}) \to r = 0_{Q}$
84	4	qusgrp	$⊢ K \in NrmSGrp (G) \to Q \in Grp$
85	13 84	syl	$⊢ φ \to Q \in Grp$
86		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
87		eqid	$⊢ 0_{Q} = 0_{Q}$
88	86 87	grpidcl	$⊢ Q \in Grp \to 0_{Q} \in {Base}_{Q}$
89	85 88	syl	$⊢ φ \to 0_{Q} \in {Base}_{Q}$
90	89	adantr	$⊢ (φ \land r = 0_{Q}) \to 0_{Q} \in {Base}_{Q}$
91	83 90	eqeltrd	$⊢ (φ \land r = 0_{Q}) \to r \in {Base}_{Q}$
92	91	ex	$⊢ φ \to (r = 0_{Q} \to r \in {Base}_{Q})$
93	92	pm4.71rd	$⊢ φ \to (r = 0_{Q} \leftrightarrow (r \in {Base}_{Q} \land r = 0_{Q}))$
94	82 93	bitr4d	$⊢ φ \to ((r \in {Base}_{Q} \land J (r) = \underset{˙}{0}) \leftrightarrow r = 0_{Q})$
95	2	adantr	$⊢ (φ \land q \in {Base}_{Q}) \to F \in (G GrpHom H)$
96	95	imaexd	$⊢ (φ \land q \in {Base}_{Q}) \to F [q] \in V$
97	96	uniexd	$⊢ (φ \land q \in {Base}_{Q}) \to ⋃ F [q] \in V$
98	5	a1i	$⊢ φ \to J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
99	22 36	fnfvelrnd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F (x) \in ran F$
100	6	ad3antrrr	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to ran F = {Base}_{H}$
101	99 100	eleqtrd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F (x) \in {Base}_{H}$
102	38 101	eqeltrd	$⊢ (((φ \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r) \in {Base}_{H}$
103	102 80	r19.29a	$⊢ (φ \land r \in {Base}_{Q}) \to J (r) \in {Base}_{H}$
104	97 98 103	fmpt2d	$⊢ φ \to J : {Base}_{Q} ⟶ {Base}_{H}$
105	104	ffnd	$⊢ φ \to J Fn {Base}_{Q}$
106		fniniseg	$⊢ J Fn {Base}_{Q} \to (r \in J^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (r \in {Base}_{Q} \land J (r) = \underset{˙}{0}))$
107	105 106	syl	$⊢ φ \to (r \in J^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (r \in {Base}_{Q} \land J (r) = \underset{˙}{0}))$
108		velsn	$⊢ r \in \{0_{Q}\} \leftrightarrow r = 0_{Q}$
109	108	a1i	$⊢ φ \to (r \in \{0_{Q}\} \leftrightarrow r = 0_{Q})$
110	94 107 109	3bitr4d	$⊢ φ \to (r \in J^{-1} [\{\underset{˙}{0}\}] \leftrightarrow r \in \{0_{Q}\})$
111	110	eqrdv	$⊢ φ \to J^{-1} [\{\underset{˙}{0}\}] = \{0_{Q}\}$
112	86 18 87 1	kerf1ghm	$⊢ J \in (Q GrpHom H) \to (J : {Base}_{Q} \underset{1-1}{⟶} {Base}_{H} \leftrightarrow J^{-1} [\{\underset{˙}{0}\}] = \{0_{Q}\})$
113	112	biimpar	$⊢ (J \in (Q GrpHom H) \land J^{-1} [\{\underset{˙}{0}\}] = \{0_{Q}\}) \to J : {Base}_{Q} \underset{1-1}{⟶} {Base}_{H}$
114	7 111 113	syl2anc	$⊢ φ \to J : {Base}_{Q} \underset{1-1}{⟶} {Base}_{H}$
115		f1f1orn	$⊢ J : {Base}_{Q} \underset{1-1}{⟶} {Base}_{H} \to J : {Base}_{Q} \underset{1-1 onto}{⟶} ran J$
116	114 115	syl	$⊢ φ \to J : {Base}_{Q} \underset{1-1 onto}{⟶} ran J$
117		simpr	$⊢ (φ \land x \in {Base}_{G}) \to x \in {Base}_{G}$
118		ovex	$⊢ G ~_{QG} K \in V$
119	118	ecelqsi	$⊢ x \in {Base}_{G} \to [x] (G ~_{QG} K) \in ({Base}_{G} / (G ~_{QG} K))$
120	117 119	syl	$⊢ (φ \land x \in {Base}_{G}) \to [x] (G ~_{QG} K) \in ({Base}_{G} / (G ~_{QG} K))$
121	27	adantr	$⊢ (φ \land x \in {Base}_{G}) \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
122	120 121	eleqtrd	$⊢ (φ \land x \in {Base}_{G}) \to [x] (G ~_{QG} K) \in {Base}_{Q}$
123		elqsi	$⊢ r \in ({Base}_{G} / (G ~_{QG} K)) \to \exists x \in {Base}_{G} r = [x] (G ~_{QG} K)$
124	51 123	syl	$⊢ (φ \land r \in {Base}_{Q}) \to \exists x \in {Base}_{G} r = [x] (G ~_{QG} K)$
125		simpr	$⊢ ((φ \land x \in {Base}_{G}) \land r = [x] (G ~_{QG} K)) \to r = [x] (G ~_{QG} K)$
126	125	fveq2d	$⊢ ((φ \land x \in {Base}_{G}) \land r = [x] (G ~_{QG} K)) \to J (r) = J ([x] (G ~_{QG} K))$
127	2	adantr	$⊢ (φ \land x \in {Base}_{G}) \to F \in (G GrpHom H)$
128	1 127 3 4 5 117	ghmquskerlem1	$⊢ (φ \land x \in {Base}_{G}) \to J ([x] (G ~_{QG} K)) = F (x)$
129	128	adantr	$⊢ ((φ \land x \in {Base}_{G}) \land r = [x] (G ~_{QG} K)) \to J ([x] (G ~_{QG} K)) = F (x)$
130	126 129	eqtrd	$⊢ ((φ \land x \in {Base}_{G}) \land r = [x] (G ~_{QG} K)) \to J (r) = F (x)$
131	130	3impa	$⊢ (φ \land x \in {Base}_{G} \land r = [x] (G ~_{QG} K)) \to J (r) = F (x)$
132	131	eqeq1d	$⊢ (φ \land x \in {Base}_{G} \land r = [x] (G ~_{QG} K)) \to (J (r) = y \leftrightarrow F (x) = y)$
133	122 124 132	rexxfrd2	$⊢ φ \to (\exists r \in {Base}_{Q} J (r) = y \leftrightarrow \exists x \in {Base}_{G} F (x) = y)$
134		fvelrnb	$⊢ J Fn {Base}_{Q} \to (y \in ran J \leftrightarrow \exists r \in {Base}_{Q} J (r) = y)$
135	105 134	syl	$⊢ φ \to (y \in ran J \leftrightarrow \exists r \in {Base}_{Q} J (r) = y)$
136		fvelrnb	$⊢ F Fn {Base}_{G} \to (y \in ran F \leftrightarrow \exists x \in {Base}_{G} F (x) = y)$
137	21 136	syl	$⊢ φ \to (y \in ran F \leftrightarrow \exists x \in {Base}_{G} F (x) = y)$
138	133 135 137	3bitr4rd	$⊢ φ \to (y \in ran F \leftrightarrow y \in ran J)$
139	138	eqrdv	$⊢ φ \to ran F = ran J$
140	139 6	eqtr3d	$⊢ φ \to ran J = {Base}_{H}$
141	140	f1oeq3d	$⊢ φ \to (J : {Base}_{Q} \underset{1-1 onto}{⟶} ran J \leftrightarrow J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H})$
142	116 141	mpbid	$⊢ φ \to J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H}$
143	86 18	isgim	$⊢ J \in (Q GrpIso H) \leftrightarrow (J \in (Q GrpHom H) \land J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H})$
144	7 142 143	sylanbrc	$⊢ φ \to J \in (Q GrpIso H)$

Metamath Proof Explorer

Theorem ghmqusker

Proof