Theorem ghmquskerco

Description: In the case of theorem ghmqusker , the composition of the natural homomorphism L with the constructed homomorphism J equals the original homomorphism F . One says that F factors through Q . (Proposed by Saveliy Skresanov, 15-Feb-2025.) (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 ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
	ghmquskerco.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ghmquskerco.l	⊢ 𝐿 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
Assertion	ghmquskerco	⊢ ( 𝜑 → 𝐹 = ( 𝐽 ∘ 𝐿 ) )

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		ghmquskerco.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
7		ghmquskerco.l	⊢ 𝐿 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
8		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9	6 8	ghmf	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
10	2 9	syl	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
11	10	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
13	12	imaexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ∈ V )
14	13	uniexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ∈ V )
15	14	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ∈ V )
16		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
17	16	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐵 ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ∈ V → ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ) Fn 𝐵 )
18	15 17	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ) Fn 𝐵 )
19		ovex	⊢ ( 𝐺 ~QG 𝐾 ) ∈ V
20	19	ecelqsi	⊢ ( 𝑥 ∈ 𝐵 → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( 𝐵 / ( 𝐺 ~QG 𝐾 ) ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( 𝐵 / ( 𝐺 ~QG 𝐾 ) ) )
22	4	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) ) )
23	6	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
24		ovexd	⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) ∈ V )
25		reldmghm	⊢ Rel dom GrpHom
26	25	ovrcl	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
27	26	simpld	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ V )
28	2 27	syl	⊢ ( 𝜑 → 𝐺 ∈ V )
29	22 23 24 28	qusbas	⊢ ( 𝜑 → ( 𝐵 / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
31	21 30	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ ( Base ‘ 𝑄 ) )
32	7	a1i	⊢ ( 𝜑 → 𝐿 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
33	5	a1i	⊢ ( 𝜑 → 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) ) )
34		imaeq2	⊢ ( 𝑞 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) → ( 𝐹 “ 𝑞 ) = ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
35	34	unieqd	⊢ ( 𝑞 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) → ∪ ( 𝐹 “ 𝑞 ) = ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
36	31 32 33 35	fmptco	⊢ ( 𝜑 → ( 𝐽 ∘ 𝐿 ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ) )
37	36	fneq1d	⊢ ( 𝜑 → ( ( 𝐽 ∘ 𝐿 ) Fn 𝐵 ↔ ( 𝑥 ∈ 𝐵 ↦ ∪ ( 𝐹 “ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) ) Fn 𝐵 ) )
38	18 37	mpbird	⊢ ( 𝜑 → ( 𝐽 ∘ 𝐿 ) Fn 𝐵 )
39		ecexg	⊢ ( ( 𝐺 ~QG 𝐾 ) ∈ V → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ V )
40	19 39	ax-mp	⊢ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ V
41	40 7	fnmpti	⊢ 𝐿 Fn 𝐵
42		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
43		fvco2	⊢ ( ( 𝐿 Fn 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐽 ∘ 𝐿 ) ‘ 𝑥 ) = ( 𝐽 ‘ ( 𝐿 ‘ 𝑥 ) ) )
44	41 42 43	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐽 ∘ 𝐿 ) ‘ 𝑥 ) = ( 𝐽 ‘ ( 𝐿 ‘ 𝑥 ) ) )
45	40	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ∈ V )
46	32 45	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐿 ‘ 𝑥 ) = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
47	46	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐽 ‘ ( 𝐿 ‘ 𝑥 ) ) = ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
48	42 6	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
49	1 12 3 4 5 48	ghmquskerlem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ 𝑥 ) )
50	44 47 49	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝐽 ∘ 𝐿 ) ‘ 𝑥 ) )
51	11 38 50	eqfnfvd	⊢ ( 𝜑 → 𝐹 = ( 𝐽 ∘ 𝐿 ) )