Metamath Proof Explorer

Theorem ghmqusnsglem2

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

Ref Expression
Hypotheses ghmqusnsg.0 
|- .0. = ( 0g ` H )
ghmqusnsg.f 
|- ( ph -> F e. ( G GrpHom H ) )
ghmqusnsg.k 
|- K = ( `' F " { .0. } )
ghmqusnsg.q 
|- Q = ( G /s ( G ~QG N ) )
ghmqusnsg.j 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
ghmqusnsg.n 
|- ( ph -> N C_ K )
ghmqusnsg.1 
|- ( ph -> N e. ( NrmSGrp ` G ) )
ghmqusnsglem2.y 
|- ( ph -> Y e. ( Base ` Q ) )
Assertion ghmqusnsglem2 
|- ( ph -> E. x e. Y ( J ` Y ) = ( F ` x ) )

Proof

Step Hyp Ref Expression
1 ghmqusnsg.0 
 |-  .0. = ( 0g ` H )
2 ghmqusnsg.f 
 |-  ( ph -> F e. ( G GrpHom H ) )
3 ghmqusnsg.k 
 |-  K = ( `' F " { .0. } )
4 ghmqusnsg.q 
 |-  Q = ( G /s ( G ~QG N ) )
5 ghmqusnsg.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
6 ghmqusnsg.n 
 |-  ( ph -> N C_ K )
7 ghmqusnsg.1 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
8 ghmqusnsglem2.y 
 |-  ( ph -> Y e. ( Base ` Q ) )
9 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG N ) ) )
10 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
11 ovexd 
 |-  ( ph -> ( G ~QG N ) e. _V )
12 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
13 2 12 syl 
 |-  ( ph -> G e. Grp )
14 9 10 11 13 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG N ) ) = ( Base ` Q ) )
15 8 14 eleqtrrd 
 |-  ( ph -> Y e. ( ( Base ` G ) /. ( G ~QG N ) ) )
16 elqsg 
 |-  ( Y e. ( Base ` Q ) -> ( Y e. ( ( Base ` G ) /. ( G ~QG N ) ) <-> E. x e. ( Base ` G ) Y = [ x ] ( G ~QG N ) ) )
17 16 biimpa 
 |-  ( ( Y e. ( Base ` Q ) /\ Y e. ( ( Base ` G ) /. ( G ~QG N ) ) ) -> E. x e. ( Base ` G ) Y = [ x ] ( G ~QG N ) )
18 8 15 17 syl2anc 
 |-  ( ph -> E. x e. ( Base ` G ) Y = [ x ] ( G ~QG N ) )
19 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
20 eqid 
 |-  ( Base ` G ) = ( Base ` G )
21 eqid 
 |-  ( G ~QG N ) = ( G ~QG N )
22 20 21 eqger 
 |-  ( N e. ( SubGrp ` G ) -> ( G ~QG N ) Er ( Base ` G ) )
23 7 19 22 3syl 
 |-  ( ph -> ( G ~QG N ) Er ( Base ` G ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> ( G ~QG N ) Er ( Base ` G ) )
25 simplr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> x e. ( Base ` G ) )
26 ecref 
 |-  ( ( ( G ~QG N ) Er ( Base ` G ) /\ x e. ( Base ` G ) ) -> x e. [ x ] ( G ~QG N ) )
27 24 25 26 syl2anc 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> x e. [ x ] ( G ~QG N ) )
28 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> Y = [ x ] ( G ~QG N ) )
29 27 28 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> x e. Y )
30 28 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> ( J ` Y ) = ( J ` [ x ] ( G ~QG N ) ) )
31 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> F e. ( G GrpHom H ) )
32 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> N C_ K )
33 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> N e. ( NrmSGrp ` G ) )
34 1 31 3 4 5 32 33 25 ghmqusnsglem1 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> ( J ` [ x ] ( G ~QG N ) ) = ( F ` x ) )
35 30 34 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> ( J ` Y ) = ( F ` x ) )
36 29 35 jca 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ Y = [ x ] ( G ~QG N ) ) -> ( x e. Y /\ ( J ` Y ) = ( F ` x ) ) )
37 36 expl 
 |-  ( ph -> ( ( x e. ( Base ` G ) /\ Y = [ x ] ( G ~QG N ) ) -> ( x e. Y /\ ( J ` Y ) = ( F ` x ) ) ) )
38 37 reximdv2 
 |-  ( ph -> ( E. x e. ( Base ` G ) Y = [ x ] ( G ~QG N ) -> E. x e. Y ( J ` Y ) = ( F ` x ) ) )
39 18 38 mpd 
 |-  ( ph -> E. x e. Y ( J ` Y ) = ( F ` x ) )