Metamath Proof Explorer

Theorem 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 ⊢ 0 = ( 0g ‘ 𝐻 )
ghmqusker.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
ghmqusker.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
ghmqusker.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
ghmqusker.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
ghmqusker.s ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
Assertion ghmqusker ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ghmqusker.1 ⊢ 0 = ( 0g ‘ 𝐻 )
2 ghmqusker.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
3 ghmqusker.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 ghmqusker.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
5 ghmqusker.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 ghmqusker.s ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
7 1 2 3 4 5 ghmquskerlem3 ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) )
8 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
9 2 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
10 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝐺 ∈ Grp )
11 1 ghmker ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) )
12 2 11 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) )
13 3 12 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) )
14 nsgsubg ⊢ ( 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
16 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
17 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
18 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
19 17 18 ghmf ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
20 2 19 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
21 20 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐺 ) )
22 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 Fn ( Base ‘ 𝐺 ) )
23 22 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝐹 Fn ( Base ‘ 𝐺 ) )
24 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) ) )
25 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
26 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) ∈ V )
27 24 25 26 9 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
28 eqid ⊢ ( 𝐺 ~QG 𝐾 ) = ( 𝐺 ~QG 𝐾 )
29 17 28 eqger ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
30 13 14 29 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
31 30 qsss ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
32 27 31 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ 𝒫 ( Base ‘ 𝐺 ) )
34 33 elpwid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
35 34 sselda ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
36 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
37 36 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
39 38 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐽 ‘ 𝑟 ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
40 39 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
41 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
42 41 biimpar ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐺 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
43 23 37 40 42 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
44 43 3 eleqtrrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑥 ∈ 𝐾 )
45 28 eqg0el ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) = 𝐾 ↔ 𝑥 ∈ 𝐾 ) )
46 45 biimpar ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝐾 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) = 𝐾 )
47 10 16 44 46 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) = 𝐾 )
48 30 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
50 27 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
51 49 50 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
52 51 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
53 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑥 ∈ 𝑟 )
54 qsel ⊢ ( ( ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) ∧ 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
55 48 52 53 54 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
56 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
57 17 28 56 eqgid ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = 𝐾 )
58 15 57 syl ⊢ ( 𝜑 → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = 𝐾 )
59 58 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = 𝐾 )
60 47 55 59 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑟 = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) )
61 4 56 qus0 ⊢ ( 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = ( 0g ‘ 𝑄 ) )
62 13 61 syl ⊢ ( 𝜑 → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = ( 0g ‘ 𝑄 ) )
63 62 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = ( 0g ‘ 𝑄 ) )
64 63 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) = ( 0g ‘ 𝑄 ) )
65 60 64 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) → 𝑟 = ( 0g ‘ 𝑄 ) )
66 63 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑟 = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) ↔ 𝑟 = ( 0g ‘ 𝑄 ) ) )
67 66 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → 𝑟 = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) )
68 67 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐽 ‘ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) ) )
69 2 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
71 17 56 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
72 9 71 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
73 72 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
74 1 70 3 4 5 73 ghmquskerlem1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 𝐽 ‘ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) )
75 56 1 ghmid ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = 0 )
76 2 75 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = 0 )
77 76 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = 0 )
78 68 74 77 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 𝐽 ‘ 𝑟 ) = 0 )
79 65 78 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐽 ‘ 𝑟 ) = 0 ↔ 𝑟 = ( 0g ‘ 𝑄 ) ) )
80 1 69 3 4 5 49 ghmquskerlem2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ 𝑟 ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
81 79 80 r19.29a ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝐽 ‘ 𝑟 ) = 0 ↔ 𝑟 = ( 0g ‘ 𝑄 ) ) )
82 81 pm5.32da ⊢ ( 𝜑 → ( ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) ↔ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) ) )
83 simpr ⊢ ( ( 𝜑 ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → 𝑟 = ( 0g ‘ 𝑄 ) )
84 4 qusgrp ⊢ ( 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑄 ∈ Grp )
85 13 84 syl ⊢ ( 𝜑 → 𝑄 ∈ Grp )
86 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
87 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
88 86 87 grpidcl ⊢ ( 𝑄 ∈ Grp → ( 0g ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
89 85 88 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → ( 0g ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
91 83 90 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
92 91 ex ⊢ ( 𝜑 → ( 𝑟 = ( 0g ‘ 𝑄 ) → 𝑟 ∈ ( Base ‘ 𝑄 ) ) )
93 92 pm4.71rd ⊢ ( 𝜑 → ( 𝑟 = ( 0g ‘ 𝑄 ) ↔ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ 𝑟 = ( 0g ‘ 𝑄 ) ) ) )
94 82 93 bitr4d ⊢ ( 𝜑 → ( ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) ↔ 𝑟 = ( 0g ‘ 𝑄 ) ) )
95 2 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
96 95 imaexd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐹 “ 𝑞 ) ∈ V )
97 96 uniexd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → ∪ ( 𝐹 “ 𝑞 ) ∈ V )
98 5 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) ) )
99 22 36 fnfvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
100 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ran 𝐹 = ( Base ‘ 𝐻 ) )
101 99 100 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐻 ) )
102 38 101 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ 𝑟 ) ∈ ( Base ‘ 𝐻 ) )
103 102 80 r19.29a ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐽 ‘ 𝑟 ) ∈ ( Base ‘ 𝐻 ) )
104 97 98 103 fmpt2d ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) ⟶ ( Base ‘ 𝐻 ) )
105 104 ffnd ⊢ ( 𝜑 → 𝐽 Fn ( Base ‘ 𝑄 ) )
106 fniniseg ⊢ ( 𝐽 Fn ( Base ‘ 𝑄 ) → ( 𝑟 ∈ ( ◡ 𝐽 “ { 0 } ) ↔ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) ) )
107 105 106 syl ⊢ ( 𝜑 → ( 𝑟 ∈ ( ◡ 𝐽 “ { 0 } ) ↔ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐽 ‘ 𝑟 ) = 0 ) ) )
108 velsn ⊢ ( 𝑟 ∈ { ( 0g ‘ 𝑄 ) } ↔ 𝑟 = ( 0g ‘ 𝑄 ) )
109 108 a1i ⊢ ( 𝜑 → ( 𝑟 ∈ { ( 0g ‘ 𝑄 ) } ↔ 𝑟 = ( 0g ‘ 𝑄 ) ) )
110 94 107 109 3bitr4d ⊢ ( 𝜑 → ( 𝑟 ∈ ( ◡ 𝐽 “ { 0 } ) ↔ 𝑟 ∈ { ( 0g ‘ 𝑄 ) } ) )
111 110 eqrdv ⊢ ( 𝜑 → ( ◡ 𝐽 “ { 0 } ) = { ( 0g ‘ 𝑄 ) } )
112 86 18 87 1 kerf1ghm ⊢ ( 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) → ( 𝐽 : ( Base ‘ 𝑄 ) –1-1→ ( Base ‘ 𝐻 ) ↔ ( ◡ 𝐽 “ { 0 } ) = { ( 0g ‘ 𝑄 ) } ) )
113 112 biimpar ⊢ ( ( 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) ∧ ( ◡ 𝐽 “ { 0 } ) = { ( 0g ‘ 𝑄 ) } ) → 𝐽 : ( Base ‘ 𝑄 ) –1-1→ ( Base ‘ 𝐻 ) )
114 7 111 113 syl2anc ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) –1-1→ ( Base ‘ 𝐻 ) )
115 f1f1orn ⊢ ( 𝐽 : ( Base ‘ 𝑄 ) –1-1→ ( Base ‘ 𝐻 ) → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ran 𝐽 )
116 114 115 syl ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ran 𝐽 )
117 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
118 ovex ⊢ ( 𝐺 ~QG 𝐾 ) ∈ V
119 118 ecelqsi ⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
120 117 119 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
121 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
122 120 121 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( Base ‘ 𝑄 ) )
123 elqsi ⊢ ( 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
124 51 123 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
125 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
126 125 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
127 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
128 1 127 3 4 5 117 ghmquskerlem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ 𝑥 ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ 𝑥 ) )
130 126 129 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
131 130 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
132 131 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( ( 𝐽 ‘ 𝑟 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
133 122 124 132 rexxfrd2 ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( Base ‘ 𝑄 ) ( 𝐽 ‘ 𝑟 ) = 𝑦 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
134 fvelrnb ⊢ ( 𝐽 Fn ( Base ‘ 𝑄 ) → ( 𝑦 ∈ ran 𝐽 ↔ ∃ 𝑟 ∈ ( Base ‘ 𝑄 ) ( 𝐽 ‘ 𝑟 ) = 𝑦 ) )
135 105 134 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐽 ↔ ∃ 𝑟 ∈ ( Base ‘ 𝑄 ) ( 𝐽 ‘ 𝑟 ) = 𝑦 ) )
136 fvelrnb ⊢ ( 𝐹 Fn ( Base ‘ 𝐺 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
137 21 136 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
138 133 135 137 3bitr4rd ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐽 ) )
139 138 eqrdv ⊢ ( 𝜑 → ran 𝐹 = ran 𝐽 )
140 139 6 eqtr3d ⊢ ( 𝜑 → ran 𝐽 = ( Base ‘ 𝐻 ) )
141 140 f1oeq3d ⊢ ( 𝜑 → ( 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ran 𝐽 ↔ 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) ) )
142 116 141 mpbid ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
143 86 18 isgim ⊢ ( 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) ↔ ( 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) ∧ 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) ) )
144 7 142 143 sylanbrc ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) )