Metamath Proof Explorer

Theorem ghmquskerlem1

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 ) )
ghmquskerlem1.x 
|- ( ph -> X e. ( Base ` G ) )
Assertion ghmquskerlem1 
|- ( ph -> ( J ` [ X ] ( G ~QG K ) ) = ( 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 ghmquskerlem1.x 
 |-  ( ph -> X e. ( Base ` G ) )
7 imaeq2 
 |-  ( q = [ X ] ( G ~QG K ) -> ( F " q ) = ( F " [ X ] ( G ~QG K ) ) )
8 7 unieqd 
 |-  ( q = [ X ] ( G ~QG K ) -> U. ( F " q ) = U. ( F " [ X ] ( G ~QG K ) ) )
9 ovex 
 |-  ( G ~QG K ) e. _V
10 9 ecelqsi 
 |-  ( X e. ( Base ` G ) -> [ X ] ( G ~QG K ) e. ( ( Base ` G ) /. ( G ~QG K ) ) )
11 6 10 syl 
 |-  ( ph -> [ X ] ( G ~QG K ) e. ( ( Base ` G ) /. ( G ~QG K ) ) )
12 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
13 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
14 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
15 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
16 2 15 syl 
 |-  ( ph -> G e. Grp )
17 12 13 14 16 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
18 11 17 eleqtrd 
 |-  ( ph -> [ X ] ( G ~QG K ) e. ( Base ` Q ) )
19 2 imaexd 
 |-  ( ph -> ( F " [ X ] ( G ~QG K ) ) e. _V )
20 19 uniexd 
 |-  ( ph -> U. ( F " [ X ] ( G ~QG K ) ) e. _V )
21 5 8 18 20 fvmptd3 
 |-  ( ph -> ( J ` [ X ] ( G ~QG K ) ) = U. ( F " [ X ] ( G ~QG K ) ) )
22 eqid 
 |-  ( Base ` G ) = ( Base ` G )
23 eqid 
 |-  ( Base ` H ) = ( Base ` H )
24 22 23 ghmf 
 |-  ( F e. ( G GrpHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
25 2 24 syl 
 |-  ( ph -> F : ( Base ` G ) --> ( Base ` H ) )
26 25 ffnd 
 |-  ( ph -> F Fn ( Base ` G ) )
27 1 ghmker 
 |-  ( F e. ( G GrpHom H ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
28 2 27 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
29 3 28 eqeltrid 
 |-  ( ph -> K e. ( NrmSGrp ` G ) )
30 nsgsubg 
 |-  ( K e. ( NrmSGrp ` G ) -> K e. ( SubGrp ` G ) )
31 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
32 22 31 eqger 
 |-  ( K e. ( SubGrp ` G ) -> ( G ~QG K ) Er ( Base ` G ) )
33 29 30 32 3syl 
 |-  ( ph -> ( G ~QG K ) Er ( Base ` G ) )
34 33 ecss 
 |-  ( ph -> [ X ] ( G ~QG K ) C_ ( Base ` G ) )
35 26 34 fvelimabd 
 |-  ( ph -> ( y e. ( F " [ X ] ( G ~QG K ) ) <-> E. z e. [ X ] ( G ~QG K ) ( F ` z ) = y ) )
36 simpr 
 |-  ( ( ( ph /\ z e. [ X ] ( G ~QG K ) ) /\ ( F ` z ) = y ) -> ( F ` z ) = y )
37 2 adantr 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> F e. ( G GrpHom H ) )
38 eqid 
 |-  ( invg ` G ) = ( invg ` G )
39 37 15 syl 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> G e. Grp )
40 6 adantr 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> X e. ( Base ` G ) )
41 22 38 39 40 grpinvcld 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( invg ` G ) ` X ) e. ( Base ` G ) )
42 34 sselda 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> z e. ( Base ` G ) )
43 eqid 
 |-  ( +g ` G ) = ( +g ` G )
44 eqid 
 |-  ( +g ` H ) = ( +g ` H )
45 22 43 44 ghmlin 
 |-  ( ( F e. ( G GrpHom H ) /\ ( ( invg ` G ) ` X ) e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) )
46 37 41 42 45 syl3anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) )
47 26 adantr 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> F Fn ( Base ` G ) )
48 22 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ ( Base ` G ) )
49 29 30 48 3syl 
 |-  ( ph -> K C_ ( Base ` G ) )
50 49 adantr 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> K C_ ( Base ` G ) )
51 vex 
 |-  z e. _V
52 elecg 
 |-  ( ( z e. _V /\ X e. ( Base ` G ) ) -> ( z e. [ X ] ( G ~QG K ) <-> X ( G ~QG K ) z ) )
53 51 52 mpan 
 |-  ( X e. ( Base ` G ) -> ( z e. [ X ] ( G ~QG K ) <-> X ( G ~QG K ) z ) )
54 53 biimpa 
 |-  ( ( X e. ( Base ` G ) /\ z e. [ X ] ( G ~QG K ) ) -> X ( G ~QG K ) z )
55 6 54 sylan 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> X ( G ~QG K ) z )
56 22 38 43 31 eqgval 
 |-  ( ( G e. Grp /\ K C_ ( Base ` G ) ) -> ( X ( G ~QG K ) z <-> ( X e. ( Base ` G ) /\ z e. ( Base ` G ) /\ ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. K ) ) )
57 56 biimpa 
 |-  ( ( ( G e. Grp /\ K C_ ( Base ` G ) ) /\ X ( G ~QG K ) z ) -> ( X e. ( Base ` G ) /\ z e. ( Base ` G ) /\ ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. K ) )
58 57 simp3d 
 |-  ( ( ( G e. Grp /\ K C_ ( Base ` G ) ) /\ X ( G ~QG K ) z ) -> ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. K )
59 39 50 55 58 syl21anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. K )
60 59 3 eleqtrdi 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( `' F " { .0. } ) )
61 fniniseg 
 |-  ( F Fn ( Base ` G ) -> ( ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( `' F " { .0. } ) <-> ( ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( Base ` G ) /\ ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = .0. ) ) )
62 61 biimpa 
 |-  ( ( F Fn ( Base ` G ) /\ ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( `' F " { .0. } ) ) -> ( ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( Base ` G ) /\ ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = .0. ) )
63 47 60 62 syl2anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) e. ( Base ` G ) /\ ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = .0. ) )
64 63 simprd 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` ( ( ( invg ` G ) ` X ) ( +g ` G ) z ) ) = .0. )
65 46 64 eqtr3d 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) = .0. )
66 65 oveq2d 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` X ) ( +g ` H ) ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) ) = ( ( F ` X ) ( +g ` H ) .0. ) )
67 eqid 
 |-  ( invg ` H ) = ( invg ` H )
68 22 38 67 ghminv 
 |-  ( ( F e. ( G GrpHom H ) /\ X e. ( Base ` G ) ) -> ( F ` ( ( invg ` G ) ` X ) ) = ( ( invg ` H ) ` ( F ` X ) ) )
69 37 40 68 syl2anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` ( ( invg ` G ) ` X ) ) = ( ( invg ` H ) ` ( F ` X ) ) )
70 69 oveq1d 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) = ( ( ( invg ` H ) ` ( F ` X ) ) ( +g ` H ) ( F ` z ) ) )
71 70 oveq2d 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` X ) ( +g ` H ) ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) ) = ( ( F ` X ) ( +g ` H ) ( ( ( invg ` H ) ` ( F ` X ) ) ( +g ` H ) ( F ` z ) ) ) )
72 ghmgrp2 
 |-  ( F e. ( G GrpHom H ) -> H e. Grp )
73 37 72 syl 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> H e. Grp )
74 37 24 syl 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> F : ( Base ` G ) --> ( Base ` H ) )
75 74 40 ffvelcdmd 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` X ) e. ( Base ` H ) )
76 74 42 ffvelcdmd 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` z ) e. ( Base ` H ) )
77 23 44 67 grpasscan1 
 |-  ( ( H e. Grp /\ ( F ` X ) e. ( Base ` H ) /\ ( F ` z ) e. ( Base ` H ) ) -> ( ( F ` X ) ( +g ` H ) ( ( ( invg ` H ) ` ( F ` X ) ) ( +g ` H ) ( F ` z ) ) ) = ( F ` z ) )
78 73 75 76 77 syl3anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` X ) ( +g ` H ) ( ( ( invg ` H ) ` ( F ` X ) ) ( +g ` H ) ( F ` z ) ) ) = ( F ` z ) )
79 71 78 eqtrd 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` X ) ( +g ` H ) ( ( F ` ( ( invg ` G ) ` X ) ) ( +g ` H ) ( F ` z ) ) ) = ( F ` z ) )
80 23 44 1 grprid 
 |-  ( ( H e. Grp /\ ( F ` X ) e. ( Base ` H ) ) -> ( ( F ` X ) ( +g ` H ) .0. ) = ( F ` X ) )
81 73 75 80 syl2anc 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( ( F ` X ) ( +g ` H ) .0. ) = ( F ` X ) )
82 66 79 81 3eqtr3d 
 |-  ( ( ph /\ z e. [ X ] ( G ~QG K ) ) -> ( F ` z ) = ( F ` X ) )
83 82 adantr 
 |-  ( ( ( ph /\ z e. [ X ] ( G ~QG K ) ) /\ ( F ` z ) = y ) -> ( F ` z ) = ( F ` X ) )
84 36 83 eqtr3d 
 |-  ( ( ( ph /\ z e. [ X ] ( G ~QG K ) ) /\ ( F ` z ) = y ) -> y = ( F ` X ) )
85 84 r19.29an 
 |-  ( ( ph /\ E. z e. [ X ] ( G ~QG K ) ( F ` z ) = y ) -> y = ( F ` X ) )
86 ecref 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ X e. ( Base ` G ) ) -> X e. [ X ] ( G ~QG K ) )
87 33 6 86 syl2anc 
 |-  ( ph -> X e. [ X ] ( G ~QG K ) )
88 87 adantr 
 |-  ( ( ph /\ y = ( F ` X ) ) -> X e. [ X ] ( G ~QG K ) )
89 fveqeq2 
 |-  ( z = X -> ( ( F ` z ) = y <-> ( F ` X ) = y ) )
90 89 adantl 
 |-  ( ( ( ph /\ y = ( F ` X ) ) /\ z = X ) -> ( ( F ` z ) = y <-> ( F ` X ) = y ) )
91 simpr 
 |-  ( ( ph /\ y = ( F ` X ) ) -> y = ( F ` X ) )
92 91 eqcomd 
 |-  ( ( ph /\ y = ( F ` X ) ) -> ( F ` X ) = y )
93 88 90 92 rspcedvd 
 |-  ( ( ph /\ y = ( F ` X ) ) -> E. z e. [ X ] ( G ~QG K ) ( F ` z ) = y )
94 85 93 impbida 
 |-  ( ph -> ( E. z e. [ X ] ( G ~QG K ) ( F ` z ) = y <-> y = ( F ` X ) ) )
95 velsn 
 |-  ( y e. { ( F ` X ) } <-> y = ( F ` X ) )
96 94 95 bitr4di 
 |-  ( ph -> ( E. z e. [ X ] ( G ~QG K ) ( F ` z ) = y <-> y e. { ( F ` X ) } ) )
97 35 96 bitrd 
 |-  ( ph -> ( y e. ( F " [ X ] ( G ~QG K ) ) <-> y e. { ( F ` X ) } ) )
98 97 eqrdv 
 |-  ( ph -> ( F " [ X ] ( G ~QG K ) ) = { ( F ` X ) } )
99 98 unieqd 
 |-  ( ph -> U. ( F " [ X ] ( G ~QG K ) ) = U. { ( F ` X ) } )
100 fvex 
 |-  ( F ` X ) e. _V
101 100 unisn 
 |-  U. { ( F ` X ) } = ( F ` X )
102 99 101 eqtrdi 
 |-  ( ph -> U. ( F " [ X ] ( G ~QG K ) ) = ( F ` X ) )
103 21 102 eqtrd 
 |-  ( ph -> ( J ` [ X ] ( G ~QG K ) ) = ( F ` X ) )