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 = ( 0_g ‘ 𝐻 )
	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 = ( 0_g ‘ 𝐻 )
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 𝐻 ) )

Metamath Proof Explorer

Theorem lmhmqusker

Proof