Metamath Proof Explorer

Theorem ghmquskerlem2

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

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

Proof

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