Theorem ghmqusker 32451

Description: A surjective group homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 15-Feb-2025.)

Hypotheses

Ref	Expression
ghmqusker.1	⊢ 0 = (0g‘𝐻)
ghmqusker.f	⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))
ghmqusker.k	⊢ 𝐾 = (◡𝐹 “ { 0 })
ghmqusker.q	⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))
ghmqusker.j	⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))
ghmqusker.s	⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))

Assertion

Ref	Expression
ghmqusker	⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpIso 𝐻))

Distinct variable groups:   𝐹,𝑞   𝐺,𝑞   𝐻,𝑞   𝐽,𝑞   𝐾,𝑞   𝑄,𝑞   𝜑,𝑞

Allowed substitution hint:   0 (𝑞)

Proof of Theorem ghmqusker

Dummy variables 𝑟 𝑥 𝑦 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2732	. . 3 ⊢ (Base‘𝑄) = (Base‘𝑄)
2		eqid 2732	. . 3 ⊢ (Base‘𝐻) = (Base‘𝐻)
3		eqid 2732	. . 3 ⊢ (+g‘𝑄) = (+g‘𝑄)
4		eqid 2732	. . 3 ⊢ (+g‘𝐻) = (+g‘𝐻)
5		ghmqusker.k	. . . . 5 ⊢ 𝐾 = (◡𝐹 “ { 0 })
6		ghmqusker.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))
7		ghmqusker.1	. . . . . . 7 ⊢ 0 = (0g‘𝐻)
8	7	ghmker 19086	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝐺))
9	6, 8	syl 17	. . . . 5 ⊢ (𝜑 → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝐺))
10	5, 9	eqeltrid 2837	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (NrmSGrp‘𝐺))
11		ghmqusker.q	. . . . 5 ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))
12	11	qusgrp 19037	. . . 4 ⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → 𝑄 ∈ Grp)
13	10, 12	syl 17	. . 3 ⊢ (𝜑 → 𝑄 ∈ Grp)
14		ghmrn 19073	. . . 4 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ran 𝐹 ∈ (SubGrp‘𝐻))
15		subgrcl 18985	. . . 4 ⊢ (ran 𝐹 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp)
16	6, 14, 15	3syl 18	. . 3 ⊢ (𝜑 → 𝐻 ∈ Grp)
17	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
18	17	imaexd 31838	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → (𝐹 “ 𝑞) ∈ V)
19	18	uniexd 7716	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → ∪ (𝐹 “ 𝑞) ∈ V)
20		ghmqusker.j	. . . . 5 ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))
21	20	a1i 11	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)))
22		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘𝑟) = (𝐹‘𝑥))
23		eqid 2732	. . . . . . . . . . . 12 ⊢ (Base‘𝐺) = (Base‘𝐺)
24	23, 2	ghmf 19064	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻))
25	6, 24	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(Base‘𝐺)⟶(Base‘𝐻))
26	25	ffnd 6706	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn (Base‘𝐺))
27	26	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝐹 Fn (Base‘𝐺))
28	11	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)))
29		eqidd 2733	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺))
30		ovexd 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ~QG 𝐾) ∈ V)
31		ghmgrp1 19062	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
32	6, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ Grp)
33	28, 29, 30, 32	qusbas 17475	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄))
34		nsgsubg 19012	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
35		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ~QG 𝐾) = (𝐺 ~QG 𝐾)
36	23, 35	eqger 19032	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝐾) Er (Base‘𝐺))
37	10, 34, 36	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ~QG 𝐾) Er (Base‘𝐺))
38	37	qsss 8757	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ⊆ 𝒫 (Base‘𝐺))
39	33, 38	eqsstrrd 4018	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑄) ⊆ 𝒫 (Base‘𝐺))
40	39	sselda 3979	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ 𝒫 (Base‘𝐺))
41	40	elpwid 4606	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ⊆ (Base‘𝐺))
42	41	sselda 3979	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) → 𝑥 ∈ (Base‘𝐺))
43	42	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝑥 ∈ (Base‘𝐺))
44	27, 43	fnfvelrnd 7070	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ ran 𝐹)
45		ghmqusker.s	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))
46	45	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ran 𝐹 = (Base‘𝐻))
47	44, 46	eleqtrd 2835	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ (Base‘𝐻))
48	22, 47	eqeltrd 2833	. . . . 5 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘𝑟) ∈ (Base‘𝐻))
49	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
50		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ (Base‘𝑄))
51	7, 49, 5, 11, 20, 50	ghmquskerlem2 32450	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ∃𝑥 ∈ 𝑟 (𝐽‘𝑟) = (𝐹‘𝑥))
52	48, 51	r19.29a 3162	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → (𝐽‘𝑟) ∈ (Base‘𝐻))
53	19, 21, 52	fmpt2d 7108	. . 3 ⊢ (𝜑 → 𝐽:(Base‘𝑄)⟶(Base‘𝐻))
54	37	ad6antr 734	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐺 ~QG 𝐾) Er (Base‘𝐺))
55	50	ad5antr 732	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ∈ (Base‘𝑄))
56	33	ad6antr 734	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄))
57	55, 56	eleqtrrd 2836	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
58		simp-4r 782	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑥 ∈ 𝑟)
59		qsel 8775	. . . . . . . . . . . 12 ⊢ (((𝐺 ~QG 𝐾) Er (Base‘𝐺) ∧ 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ∧ 𝑥 ∈ 𝑟) → 𝑟 = [𝑥](𝐺 ~QG 𝐾))
60	54, 57, 58, 59	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 = [𝑥](𝐺 ~QG 𝐾))
61		simp-5r 784	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ∈ (Base‘𝑄))
62	61, 56	eleqtrrd 2836	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
63		simplr 767	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑦 ∈ 𝑠)
64		qsel 8775	. . . . . . . . . . . 12 ⊢ (((𝐺 ~QG 𝐾) Er (Base‘𝐺) ∧ 𝑠 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ∧ 𝑦 ∈ 𝑠) → 𝑠 = [𝑦](𝐺 ~QG 𝐾))
65	54, 62, 63, 64	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 = [𝑦](𝐺 ~QG 𝐾))
66	60, 65	oveq12d 7412	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝑟(+g‘𝑄)𝑠) = ([𝑥](𝐺 ~QG 𝐾)(+g‘𝑄)[𝑦](𝐺 ~QG 𝐾)))
67	10	ad6antr 734	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐾 ∈ (NrmSGrp‘𝐺))
68	41	ad5antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ⊆ (Base‘𝐺))
69	68, 58	sseldd 3980	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑥 ∈ (Base‘𝐺))
70	39	sselda 3979	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ∈ 𝒫 (Base‘𝐺))
71	70	elpwid 4606	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ⊆ (Base‘𝐺))
72	71	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ⊆ (Base‘𝐺))
73	72	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ⊆ (Base‘𝐺))
74	73, 63	sseldd 3980	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑦 ∈ (Base‘𝐺))
75		eqid 2732	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
76	11, 23, 75, 3	qusadd 19039	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ (NrmSGrp‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ([𝑥](𝐺 ~QG 𝐾)(+g‘𝑄)[𝑦](𝐺 ~QG 𝐾)) = [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝐾))
77	67, 69, 74, 76	syl3anc 1371	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ([𝑥](𝐺 ~QG 𝐾)(+g‘𝑄)[𝑦](𝐺 ~QG 𝐾)) = [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝐾))
78	66, 77	eqtrd 2772	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝑟(+g‘𝑄)𝑠) = [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝐾))
79	78	fveq2d 6883	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = (𝐽‘[(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝐾)))
80	6	ad6antr 734	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
81	80, 31	syl 17	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐺 ∈ Grp)
82	23, 75, 81, 69, 74	grpcld 18810	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
83	7, 80, 5, 11, 20, 82	ghmquskerlem1 32448	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘[(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝐾)) = (𝐹‘(𝑥(+g‘𝐺)𝑦)))
84	23, 75, 4	ghmlin 19065	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝐹‘(𝑥(+g‘𝐺)𝑦)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝑦)))
85	80, 69, 74, 84	syl3anc 1371	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐹‘(𝑥(+g‘𝐺)𝑦)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝑦)))
86	79, 83, 85	3eqtrd 2776	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝑦)))
87		simpllr 774	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘𝑟) = (𝐹‘𝑥))
88		simpr 485	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘𝑠) = (𝐹‘𝑦))
89	87, 88	oveq12d 7412	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ((𝐽‘𝑟)(+g‘𝐻)(𝐽‘𝑠)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝑦)))
90	86, 89	eqtr4d 2775	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = ((𝐽‘𝑟)(+g‘𝐻)(𝐽‘𝑠)))
91	49	ad3antrrr 728	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
92		simpllr 774	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝑠 ∈ (Base‘𝑄))
93	7, 91, 5, 11, 20, 92	ghmquskerlem2 32450	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ∃𝑦 ∈ 𝑠 (𝐽‘𝑠) = (𝐹‘𝑦))
94	90, 93	r19.29a 3162	. . . . 5 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = ((𝐽‘𝑟)(+g‘𝐻)(𝐽‘𝑠)))
95	51	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → ∃𝑥 ∈ 𝑟 (𝐽‘𝑟) = (𝐹‘𝑥))
96	94, 95	r19.29a 3162	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = ((𝐽‘𝑟)(+g‘𝐻)(𝐽‘𝑠)))
97	96	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ (Base‘𝑄) ∧ 𝑠 ∈ (Base‘𝑄))) → (𝐽‘(𝑟(+g‘𝑄)𝑠)) = ((𝐽‘𝑟)(+g‘𝐻)(𝐽‘𝑠)))
98	1, 2, 3, 4, 13, 16, 53, 97	isghmd 19069	. 2 ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻))
99	32	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐺 ∈ Grp)
100	10, 34	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
101	100	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐾 ∈ (SubGrp‘𝐺))
102	27	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐹 Fn (Base‘𝐺))
103	43	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ (Base‘𝐺))
104	22	eqeq1d 2734	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ((𝐽‘𝑟) = 0 ↔ (𝐹‘𝑥) = 0 ))
105	104	biimpa 477	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → (𝐹‘𝑥) = 0 )
106		fniniseg 7047	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝐺) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝐹‘𝑥) = 0 )))
107	106	biimpar 478	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn (Base‘𝐺) ∧ (𝑥 ∈ (Base‘𝐺) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 }))
108	102, 103, 105, 107	syl12anc 835	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ (◡𝐹 “ { 0 }))
109	108, 5	eleqtrrdi 2844	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ 𝐾)
110	35	eqg0el 32399	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝐾 ∈ (SubGrp‘𝐺)) → ([𝑥](𝐺 ~QG 𝐾) = 𝐾 ↔ 𝑥 ∈ 𝐾))
111	110	biimpar 478	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ Grp ∧ 𝐾 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝐾) → [𝑥](𝐺 ~QG 𝐾) = 𝐾)
112	99, 101, 109, 111	syl21anc 836	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → [𝑥](𝐺 ~QG 𝐾) = 𝐾)
113	37	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → (𝐺 ~QG 𝐾) Er (Base‘𝐺))
114	33	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄))
115	50, 114	eleqtrrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
116	115	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
117		simpllr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ 𝑟)
118	113, 116, 117, 59	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = [𝑥](𝐺 ~QG 𝐾))
119		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝐺) = (0g‘𝐺)
120	23, 35, 119	eqgid 19034	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾)
121	100, 120	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → [(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾)
122	121	ad4antr 730	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾)
123	112, 118, 122	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾))
124	11, 119	qus0 19040	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄))
125	10, 124	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → [(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄))
126	125	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄))
127	126	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄))
128	123, 127	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = (0g‘𝑄))
129	126	eqeq2d 2743	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾) ↔ 𝑟 = (0g‘𝑄)))
130	129	biimpar 478	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → 𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾))
131	130	fveq2d 6883	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘𝑟) = (𝐽‘[(0g‘𝐺)](𝐺 ~QG 𝐾)))
132	49	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
133	23, 119	grpidcl 18827	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ (Base‘𝐺))
134	32, 133	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐺) ∈ (Base‘𝐺))
135	134	ad4antr 730	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (0g‘𝐺) ∈ (Base‘𝐺))
136	7, 132, 5, 11, 20, 135	ghmquskerlem1 32448	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘[(0g‘𝐺)](𝐺 ~QG 𝐾)) = (𝐹‘(0g‘𝐺)))
137	119, 7	ghmid 19066	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐹‘(0g‘𝐺)) = 0 )
138	6, 137	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘(0g‘𝐺)) = 0 )
139	138	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐹‘(0g‘𝐺)) = 0 )
140	131, 136, 139	3eqtrd 2776	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘𝑟) = 0 )
141	128, 140	impbida 799	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ((𝐽‘𝑟) = 0 ↔ 𝑟 = (0g‘𝑄)))
142	141, 51	r19.29a 3162	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ((𝐽‘𝑟) = 0 ↔ 𝑟 = (0g‘𝑄)))
143	142	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ) ↔ (𝑟 ∈ (Base‘𝑄) ∧ 𝑟 = (0g‘𝑄))))
144		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → 𝑟 = (0g‘𝑄))
145		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (0g‘𝑄) = (0g‘𝑄)
146	1, 145	grpidcl 18827	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ Grp → (0g‘𝑄) ∈ (Base‘𝑄))
147	13, 146	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘𝑄) ∈ (Base‘𝑄))
148	147	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → (0g‘𝑄) ∈ (Base‘𝑄))
149	144, 148	eqeltrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → 𝑟 ∈ (Base‘𝑄))
150	149	ex 413	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 = (0g‘𝑄) → 𝑟 ∈ (Base‘𝑄)))
151	150	pm4.71rd 563	. . . . . . . 8 ⊢ (𝜑 → (𝑟 = (0g‘𝑄) ↔ (𝑟 ∈ (Base‘𝑄) ∧ 𝑟 = (0g‘𝑄))))
152	143, 151	bitr4d 281	. . . . . . 7 ⊢ (𝜑 → ((𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ) ↔ 𝑟 = (0g‘𝑄)))
153	53	ffnd 6706	. . . . . . . 8 ⊢ (𝜑 → 𝐽 Fn (Base‘𝑄))
154		fniniseg 7047	. . . . . . . 8 ⊢ (𝐽 Fn (Base‘𝑄) → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ (𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 )))
155	153, 154	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ (𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 )))
156		velsn 4639	. . . . . . . 8 ⊢ (𝑟 ∈ {(0g‘𝑄)} ↔ 𝑟 = (0g‘𝑄))
157	156	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ {(0g‘𝑄)} ↔ 𝑟 = (0g‘𝑄)))
158	152, 155, 157	3bitr4d 310	. . . . . 6 ⊢ (𝜑 → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ 𝑟 ∈ {(0g‘𝑄)}))
159	158	eqrdv 2730	. . . . 5 ⊢ (𝜑 → (◡𝐽 “ { 0 }) = {(0g‘𝑄)})
160	1, 2, 145, 7	kerf1ghm 20234	. . . . . 6 ⊢ (𝐽 ∈ (𝑄 GrpHom 𝐻) → (𝐽:(Base‘𝑄)–1-1→(Base‘𝐻) ↔ (◡𝐽 “ { 0 }) = {(0g‘𝑄)}))
161	160	biimpar 478	. . . . 5 ⊢ ((𝐽 ∈ (𝑄 GrpHom 𝐻) ∧ (◡𝐽 “ { 0 }) = {(0g‘𝑄)}) → 𝐽:(Base‘𝑄)–1-1→(Base‘𝐻))
162	98, 159, 161	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1→(Base‘𝐻))
163		f1f1orn 6832	. . . 4 ⊢ (𝐽:(Base‘𝑄)–1-1→(Base‘𝐻) → 𝐽:(Base‘𝑄)–1-1-onto→ran 𝐽)
164	162, 163	syl 17	. . 3 ⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1-onto→ran 𝐽)
165		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺))
166		ovex 7427	. . . . . . . . . . 11 ⊢ (𝐺 ~QG 𝐾) ∈ V
167	166	ecelqsi 8752	. . . . . . . . . 10 ⊢ (𝑥 ∈ (Base‘𝐺) → [𝑥](𝐺 ~QG 𝐾) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
168	165, 167	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → [𝑥](𝐺 ~QG 𝐾) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)))
169	33	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄))
170	168, 169	eleqtrd 2835	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → [𝑥](𝐺 ~QG 𝐾) ∈ (Base‘𝑄))
171		elqsi 8749	. . . . . . . . 9 ⊢ (𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) → ∃𝑥 ∈ (Base‘𝐺)𝑟 = [𝑥](𝐺 ~QG 𝐾))
172	115, 171	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ∃𝑥 ∈ (Base‘𝐺)𝑟 = [𝑥](𝐺 ~QG 𝐾))
173		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → 𝑟 = [𝑥](𝐺 ~QG 𝐾))
174	173	fveq2d 6883	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐽‘[𝑥](𝐺 ~QG 𝐾)))
175	6	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
176	7, 175, 5, 11, 20, 165	ghmquskerlem1 32448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → (𝐽‘[𝑥](𝐺 ~QG 𝐾)) = (𝐹‘𝑥))
177	176	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘[𝑥](𝐺 ~QG 𝐾)) = (𝐹‘𝑥))
178	174, 177	eqtrd 2772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐹‘𝑥))
179	178	3impa 1110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐹‘𝑥))
180	179	eqeq1d 2734	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → ((𝐽‘𝑟) = 𝑦 ↔ (𝐹‘𝑥) = 𝑦))
181	170, 172, 180	rexxfrd2 5405	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦))
182		fvelrnb 6940	. . . . . . . 8 ⊢ (𝐽 Fn (Base‘𝑄) → (𝑦 ∈ ran 𝐽 ↔ ∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦))
183	153, 182	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝐽 ↔ ∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦))
184		fvelrnb 6940	. . . . . . . 8 ⊢ (𝐹 Fn (Base‘𝐺) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦))
185	26, 184	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦))
186	181, 183, 185	3bitr4rd 311	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐽))
187	186	eqrdv 2730	. . . . 5 ⊢ (𝜑 → ran 𝐹 = ran 𝐽)
188	187, 45	eqtr3d 2774	. . . 4 ⊢ (𝜑 → ran 𝐽 = (Base‘𝐻))
189	188	f1oeq3d 6818	. . 3 ⊢ (𝜑 → (𝐽:(Base‘𝑄)–1-1-onto→ran 𝐽 ↔ 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻)))
190	164, 189	mpbid 231	. 2 ⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻))
191	1, 2	isgim 19104	. 2 ⊢ (𝐽 ∈ (𝑄 GrpIso 𝐻) ↔ (𝐽 ∈ (𝑄 GrpHom 𝐻) ∧ 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻)))
192	98, 190, 191	sylanbrc 583	1 ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpIso 𝐻))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∃wrex 3070  Vcvv 3474   ⊆ wss 3945  𝒫 cpw 4597  {csn 4623  ∪ cuni 4902   ↦ cmpt 5225  ^◡ccnv 5669  ran crn 5671   “ cima 5673   Fn wfn 6528  ⟶wf 6529  –1-1→wf1 6530  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7394   Er wer 8685  [cec 8686   / cqs 8687  Basecbs 17128  +_gcplusg 17181  0_gc0g 17369   /_s cqus 17435  Grpcgrp 18796  SubGrpcsubg 18974  NrmSGrpcnsg 18975   ~_QG cqg 18976   GrpHom cghm 19057   GrpIso cgim 19099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-om 7840  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-er 8688  df-ec 8690  df-qs 8694  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-sup 9421  df-inf 9422  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-5 12262  df-6 12263  df-7 12264  df-8 12265  df-9 12266  df-n0 12457  df-z 12543  df-dec 12662  df-uz 12807  df-fz 13469  df-struct 17064  df-sets 17081  df-slot 17099  df-ndx 17111  df-base 17129  df-ress 17158  df-plusg 17194  df-mulr 17195  df-sca 17197  df-vsca 17198  df-ip 17199  df-tset 17200  df-ple 17201  df-ds 17203  df-0g 17371  df-imas 17438  df-qus 17439  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-submnd 18650  df-grp 18799  df-minusg 18800  df-sbg 18801  df-subg 18977  df-nsg 18978  df-eqg 18979  df-ghm 19058  df-gim 19101

This theorem is referenced by:  gicqusker  32452  lmhmqusker  32453  rhmqusker  32459