Metamath Proof Explorer

Theorem ghmqusnsglem1

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