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

Metamath Proof Explorer

Theorem ghmqusnsglem2

Description: Lemma for ghmqusnsg . (Contributed by Thierry Arnoux, 13-May-2025)

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

Proof

Step Hyp Ref Expression
1 ghmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
2 ghmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
3 ghmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 ghmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
5 ghmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 ghmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
7 ghmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
8 ghmqusnsglem2.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑄 ) )
9 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
10 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
11 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) ∈ V )
12 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
13 2 12 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
14 9 10 11 13 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
15 8 14 eleqtrrd ⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
16 elqsg ⊢ ( 𝑌 ∈ ( Base ‘ 𝑄 ) → ( 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) )
17 16 biimpa ⊢ ( ( 𝑌 ∈ ( Base ‘ 𝑄 ) ∧ 𝑌 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
18 8 15 17 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
19 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
20 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
21 eqid ⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
22 20 21 eqger ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
23 7 19 22 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
26 ecref ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
27 24 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑥 ∈ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
29 27 28 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑥 ∈ 𝑌 )
30 28 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐽 ‘ 𝑌 ) = ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
32 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑁 ⊆ 𝐾 )
33 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
34 1 31 3 4 5 32 33 25 ghmqusnsglem1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐽 ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑥 ) )
35 30 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) )
36 29 35 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝑥 ∈ 𝑌 ∧ ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) )
37 36 expl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝑥 ∈ 𝑌 ∧ ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
38 37 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑌 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) → ∃ 𝑥 ∈ 𝑌 ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) )
39 18 38 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ( 𝐽 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) )