This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) )