Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ghmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
2 ghmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
3 ghmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 ghmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
5 ghmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 ghmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
7 ghmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
8 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
9 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
10 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
11 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
12 4 qusgrp ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑄 ∈ Grp )
13 7 12 syl ⊢ ( 𝜑 → 𝑄 ∈ Grp )
14 ghmrn ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ran 𝐹 ∈ ( SubGrp ‘ 𝐻 ) )
15 subgrcl ⊢ ( ran 𝐹 ∈ ( SubGrp ‘ 𝐻 ) → 𝐻 ∈ Grp )
16 2 14 15 3syl ⊢ ( 𝜑 → 𝐻 ∈ Grp )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
18 17 imaexd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐹 “ 𝑞 ) ∈ V )
19 18 uniexd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ 𝑄 ) ) → ∪ ( 𝐹 “ 𝑞 ) ∈ V )
20 5 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) ) )
21 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
22 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23 22 9 ghmf ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
24 2 23 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
25 24 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐻 ) )
26 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝐻 ) )
27 24 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐺 ) )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 Fn ( Base ‘ 𝐺 ) )
29 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
30 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
31 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) ∈ V )
32 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
33 2 32 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
34 29 30 31 33 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
35 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
36 eqid ⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
37 22 36 eqger ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
38 7 35 37 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
39 38 qsss ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
40 34 39 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
41 40 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ 𝒫 ( Base ‘ 𝐺 ) )
42 41 elpwid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
43 42 sselda ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
44 43 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
45 28 44 fnfvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
46 26 45 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐻 ) )
47 21 46 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ 𝑟 ) ∈ ( Base ‘ 𝐻 ) )
48 2 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
49 6 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑁 ⊆ 𝐾 )
50 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
52 1 48 3 4 5 49 50 51 ghmqusnsglem2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ 𝑟 ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
53 47 52 r19.29a ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐽 ‘ 𝑟 ) ∈ ( Base ‘ 𝐻 ) )
54 19 20 53 fmpt2d ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) ⟶ ( Base ‘ 𝐻 ) )
55 38 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
56 51 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
57 34 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
58 56 57 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
59 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ 𝑟 )
60 qsel ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
61 55 58 59 60 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
62 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ∈ ( Base ‘ 𝑄 ) )
63 62 57 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
64 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ 𝑠 )
65 qsel ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ∧ 𝑦 ∈ 𝑠 ) → 𝑠 = [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) )
66 55 63 64 65 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 = [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) )
67 61 66 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) = ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) )
68 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
69 42 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
70 69 59 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
71 40 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ∈ 𝒫 ( Base ‘ 𝐺 ) )
72 71 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
73 72 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
74 73 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
75 74 64 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
76 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
77 4 22 76 10 qusadd ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
78 68 70 75 77 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
79 67 78 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
80 79 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( 𝐽 ‘ [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) ) )
81 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
82 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑁 ⊆ 𝐾 )
83 81 32 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐺 ∈ Grp )
84 22 76 83 70 75 grpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
85 1 81 3 4 5 82 68 84 ghmqusnsglem1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
86 22 76 11 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
87 81 70 75 86 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
88 80 85 87 3eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
89 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
90 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) )
91 89 90 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐽 ‘ 𝑟 ) ( +g ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
92 88 91 eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( +g ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
93 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
94 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑁 ⊆ 𝐾 )
95 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
96 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑠 ∈ ( Base ‘ 𝑄 ) )
97 1 93 3 4 5 94 95 96 ghmqusnsglem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑠 ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) )
98 92 97 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( +g ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
99 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ 𝑟 ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
100 98 99 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( +g ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
101 100 anasss ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝐽 ‘ ( 𝑟 ( +g ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( +g ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
102 8 9 10 11 13 16 54 101 isghmd ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) )