Theorem ghmquskerlem2

Description: Lemma for ghmqusker . (Contributed by Thierry Arnoux, 14-Feb-2025)

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

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		ghmquskerlem2.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑄 ) )
7	4	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) ) )
8		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
9		ovexd	⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) ∈ V )
10		ghmgrp1	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
11	2 10	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
12	7 8 9 11	qusbas	⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) = ( Base ‘ 𝑄 ) )
13	6 12	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) )
14		elqsg	⊢ ( 𝑌 ∈ ( Base ‘ 𝑄 ) → ( 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
15	14	biimpa	⊢ ( ( 𝑌 ∈ ( Base ‘ 𝑄 ) ∧ 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝐾 ) ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
16	6 13 15	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
17	1	ghmker	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) )
18		nsgsubg	⊢ ( ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝐺 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( SubGrp ‘ 𝐺 ) )
19	2 17 18	3syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) ∈ ( SubGrp ‘ 𝐺 ) )
20	3 19	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
21		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22		eqid	⊢ ( 𝐺 ~QG 𝐾 ) = ( 𝐺 ~QG 𝐾 )
23	21 22	eqger	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
24	20 23	syl	⊢ ( 𝜑 → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
25	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) )
26		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
27		ecref	⊢ ( ( ( 𝐺 ~QG 𝐾 ) Er ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
28	25 26 27	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝑥 ∈ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
29		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) )
30	28 29	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝑥 ∈ 𝑌 )
31	29	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ 𝑌 ) = ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) )
32	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
33	1 32 3 4 5 26	ghmquskerlem1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) = ( 𝐹 ‘ 𝑥 ) )
34	31 33	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) )
35	30 34	jca	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝑥 ∈ 𝑌 ∧ ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) )
36	35	expl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) ) → ( 𝑥 ∈ 𝑌 ∧ ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
37	36	reximdv2	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝐾 ) → ∃ 𝑥 ∈ 𝑌 ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) )
38	16 37	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) )