Metamath Proof Explorer

Theorem lmhmqusker

Description: A surjective module 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, 25-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 lmhmqusker.1 ⊢ 0 = ( 0g ‘ 𝐻 )
2 lmhmqusker.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) )
3 lmhmqusker.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 lmhmqusker.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
5 lmhmqusker.s ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
6 lmhmqusker.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
7 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
8 eqid ⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 )
9 eqid ⊢ ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ 𝐻 )
10 eqid ⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
11 eqid ⊢ ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝐻 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) → 𝐺 ∈ LMod )
15 2 14 syl ⊢ ( 𝜑 → 𝐺 ∈ LMod )
16 eqid ⊢ ( LSubSp ‘ 𝐺 ) = ( LSubSp ‘ 𝐺 )
17 3 1 16 lmhmkerlss ⊢ ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) → 𝐾 ∈ ( LSubSp ‘ 𝐺 ) )
18 2 17 syl ⊢ ( 𝜑 → 𝐾 ∈ ( LSubSp ‘ 𝐺 ) )
19 4 13 15 18 quslmod ⊢ ( 𝜑 → 𝑄 ∈ LMod )
20 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) → 𝐻 ∈ LMod )
21 2 20 syl ⊢ ( 𝜑 → 𝐻 ∈ LMod )
22 eqid ⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
23 22 11 lmhmsca ⊢ ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) → ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝐺 ) )
24 2 23 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝐺 ) )
25 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) ) )
26 13 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
27 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) ∈ V )
28 25 26 27 15 22 quss ⊢ ( 𝜑 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑄 ) )
29 24 28 eqtrd ⊢ ( 𝜑 → ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝑄 ) )
30 lmghm ⊢ ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
31 2 30 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
32 1 31 3 4 6 5 ghmqusker ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) )
33 gimghm ⊢ ( 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) → 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) )
34 32 33 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) )
35 1 ghmker ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) )
36 31 35 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) )
37 3 36 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) )
38 nsgsubg ⊢ ( 𝐾 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
39 eqid ⊢ ( 𝐺 ~QG 𝐾 ) = ( 𝐺 ~QG 𝐾 )
40 13 39 eqger ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
41 37 38 40 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
42 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
43 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
44 25 26 27 15 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
45 44 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
46 43 45 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
47 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ 𝑟 )
48 qsel ⊢ ( ( ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) ∧ 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
49 42 46 47 48 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
50 49 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) = ( 𝑘 ( ·𝑠 ‘ 𝑄 ) [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
51 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) )
52 eqid ⊢ ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝐺 )
53 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐺 ∈ LMod )
54 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐾 ∈ ( LSubSp ‘ 𝐺 ) )
55 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
56 28 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
57 56 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
58 55 57 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) )
59 41 qsss ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
60 44 59 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
61 60 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ 𝒫 ( Base ‘ 𝐺 ) )
62 61 elpwid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
63 62 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
64 63 47 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
65 13 39 51 52 53 54 58 4 8 64 qusvsval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑄 ) [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) = [ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ] ( 𝐺 ~QG 𝐾 ) )
66 50 65 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) = [ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ] ( 𝐺 ~QG 𝐾 ) )
67 66 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) ) = ( 𝐽 ‘ [ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ] ( 𝐺 ~QG 𝐾 ) ) )
68 31 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
69 13 22 52 51 lmodvscl ⊢ ( ( 𝐺 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
70 53 58 64 69 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
71 1 68 3 4 6 70 ghmquskerlem1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ [ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ) )
72 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) )
73 22 51 13 52 9 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
74 72 58 64 73 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝐺 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
75 67 71 74 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
76 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
77 76 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐽 ‘ 𝑟 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
78 75 77 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐽 ‘ 𝑟 ) ) )
79 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
80 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
81 1 79 3 4 6 80 ghmquskerlem2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ 𝑟 ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
82 78 81 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐽 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐽 ‘ 𝑟 ) ) )
83 82 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝐽 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑄 ) 𝑟 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝐽 ‘ 𝑟 ) ) )
84 7 8 9 10 11 12 19 21 29 34 83 islmhmd ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 LMHom 𝐻 ) )
85 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
86 7 85 gimf1o ⊢ ( 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
87 32 86 syl ⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
88 7 85 islmim ⊢ ( 𝐽 ∈ ( 𝑄 LMIso 𝐻 ) ↔ ( 𝐽 ∈ ( 𝑄 LMHom 𝐻 ) ∧ 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) ) )
89 84 87 88 sylanbrc ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 LMIso 𝐻 ) )