Metamath Proof Explorer

Theorem ghmquskerlem3

Description: The mapping H induced by a surjective group homomorphism F from the quotient group Q over 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, 22-Mar-2025)

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

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