Metamath Proof Explorer

Theorem ghmquskerlem3

Description: The mapping H induced by a surjective group homomorphism F from the quotient group Q over F 's kernel K is a group isomorphism. In this case, one says that F factors through Q , which is also called the factor group. (Contributed by Thierry Arnoux, 22-Mar-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 ) )
Assertion ghmquskerlem3 
|- ( ph -> J e. ( Q GrpHom H ) )

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 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
7 eqid 
 |-  ( Base ` H ) = ( Base ` H )
8 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
9 eqid 
 |-  ( +g ` H ) = ( +g ` H )
10 1 ghmker 
 |-  ( F e. ( G GrpHom H ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
11 2 10 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
12 3 11 eqeltrid 
 |-  ( ph -> K e. ( NrmSGrp ` G ) )
13 4 qusgrp 
 |-  ( K e. ( NrmSGrp ` G ) -> Q e. Grp )
14 12 13 syl 
 |-  ( ph -> Q e. Grp )
15 ghmrn 
 |-  ( F e. ( G GrpHom H ) -> ran F e. ( SubGrp ` H ) )
16 subgrcl 
 |-  ( ran F e. ( SubGrp ` H ) -> H e. Grp )
17 2 15 16 3syl 
 |-  ( ph -> H e. Grp )
18 2 adantr 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
19 18 imaexd 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> ( F " q ) e. _V )
20 19 uniexd 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> U. ( F " q ) e. _V )
21 5 a1i 
 |-  ( ph -> J = ( q e. ( Base ` Q ) |-> U. ( F " q ) ) )
22 simpr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` r ) = ( F ` x ) )
23 eqid 
 |-  ( Base ` G ) = ( Base ` G )
24 23 7 ghmf 
 |-  ( F e. ( G GrpHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
25 2 24 syl 
 |-  ( ph -> F : ( Base ` G ) --> ( Base ` H ) )
26 25 frnd 
 |-  ( ph -> ran F C_ ( Base ` H ) )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ran F C_ ( Base ` H ) )
28 25 ffnd 
 |-  ( ph -> F Fn ( Base ` G ) )
29 28 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F Fn ( Base ` G ) )
30 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
31 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
32 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
33 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
34 2 33 syl 
 |-  ( ph -> G e. Grp )
35 30 31 32 34 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
36 nsgsubg 
 |-  ( K e. ( NrmSGrp ` G ) -> K e. ( SubGrp ` G ) )
37 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
38 23 37 eqger 
 |-  ( K e. ( SubGrp ` G ) -> ( G ~QG K ) Er ( Base ` G ) )
39 12 36 38 3syl 
 |-  ( ph -> ( G ~QG K ) Er ( Base ` G ) )
40 39 qsss 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) C_ ~P ( Base ` G ) )
41 35 40 eqsstrrd 
 |-  ( ph -> ( Base ` Q ) C_ ~P ( Base ` G ) )
42 41 sselda 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ~P ( Base ` G ) )
43 42 elpwid 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r C_ ( Base ` G ) )
44 43 sselda 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) -> x e. ( Base ` G ) )
45 44 adantr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> x e. ( Base ` G ) )
46 29 45 fnfvelrnd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( F ` x ) e. ran F )
47 27 46 sseldd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( F ` x ) e. ( Base ` H ) )
48 22 47 eqeltrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` r ) e. ( Base ` H ) )
49 2 adantr 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
50 simpr 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ( Base ` Q ) )
51 1 49 3 4 5 50 ghmquskerlem2 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> E. x e. r ( J ` r ) = ( F ` x ) )
52 48 51 r19.29a 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> ( J ` r ) e. ( Base ` H ) )
53 20 21 52 fmpt2d 
 |-  ( ph -> J : ( Base ` Q ) --> ( Base ` H ) )
54 39 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( G ~QG K ) Er ( Base ` G ) )
55 50 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> r e. ( Base ` Q ) )
56 35 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
57 55 56 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> r e. ( ( Base ` G ) /. ( G ~QG K ) ) )
58 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> x e. r )
59 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ r e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ x e. r ) -> r = [ x ] ( G ~QG K ) )
60 54 57 58 59 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> r = [ x ] ( G ~QG K ) )
61 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> s e. ( Base ` Q ) )
62 61 56 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> s e. ( ( Base ` G ) /. ( G ~QG K ) ) )
63 simplr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> y e. s )
64 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ s e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ y e. s ) -> s = [ y ] ( G ~QG K ) )
65 54 62 63 64 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> s = [ y ] ( G ~QG K ) )
66 60 65 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( r ( +g ` Q ) s ) = ( [ x ] ( G ~QG K ) ( +g ` Q ) [ y ] ( G ~QG K ) ) )
67 12 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> K e. ( NrmSGrp ` G ) )
68 43 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> r C_ ( Base ` G ) )
69 68 58 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> x e. ( Base ` G ) )
70 41 sselda 
 |-  ( ( ph /\ s e. ( Base ` Q ) ) -> s e. ~P ( Base ` G ) )
71 70 elpwid 
 |-  ( ( ph /\ s e. ( Base ` Q ) ) -> s C_ ( Base ` G ) )
72 71 adantlr 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> s C_ ( Base ` G ) )
73 72 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> s C_ ( Base ` G ) )
74 73 63 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> y e. ( Base ` G ) )
75 eqid 
 |-  ( +g ` G ) = ( +g ` G )
76 4 23 75 8 qusadd 
 |-  ( ( K e. ( NrmSGrp ` G ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( [ x ] ( G ~QG K ) ( +g ` Q ) [ y ] ( G ~QG K ) ) = [ ( x ( +g ` G ) y ) ] ( G ~QG K ) )
77 67 69 74 76 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( [ x ] ( G ~QG K ) ( +g ` Q ) [ y ] ( G ~QG K ) ) = [ ( x ( +g ` G ) y ) ] ( G ~QG K ) )
78 66 77 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( r ( +g ` Q ) s ) = [ ( x ( +g ` G ) y ) ] ( G ~QG K ) )
79 78 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( J ` [ ( x ( +g ` G ) y ) ] ( G ~QG K ) ) )
80 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> F e. ( G GrpHom H ) )
81 80 33 syl 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> G e. Grp )
82 23 75 81 69 74 grpcld 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
83 1 80 3 4 5 82 ghmquskerlem1 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` [ ( x ( +g ` G ) y ) ] ( G ~QG K ) ) = ( F ` ( x ( +g ` G ) y ) ) )
84 23 75 9 ghmlin 
 |-  ( ( F e. ( G GrpHom H ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( F ` ( x ( +g ` G ) y ) ) = ( ( F ` x ) ( +g ` H ) ( F ` y ) ) )
85 80 69 74 84 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( F ` ( x ( +g ` G ) y ) ) = ( ( F ` x ) ( +g ` H ) ( F ` y ) ) )
86 79 83 85 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( ( F ` x ) ( +g ` H ) ( F ` y ) ) )
87 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` r ) = ( F ` x ) )
88 simpr 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` s ) = ( F ` y ) )
89 87 88 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( ( J ` r ) ( +g ` H ) ( J ` s ) ) = ( ( F ` x ) ( +g ` H ) ( F ` y ) ) )
90 86 89 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( ( J ` r ) ( +g ` H ) ( J ` s ) ) )
91 2 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F e. ( G GrpHom H ) )
92 simpllr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> s e. ( Base ` Q ) )
93 1 91 3 4 5 92 ghmquskerlem2 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> E. y e. s ( J ` s ) = ( F ` y ) )
94 90 93 r19.29a 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( ( J ` r ) ( +g ` H ) ( J ` s ) ) )
95 51 adantr 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> E. x e. r ( J ` r ) = ( F ` x ) )
96 94 95 r19.29a 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( ( J ` r ) ( +g ` H ) ( J ` s ) ) )
97 96 anasss 
 |-  ( ( ph /\ ( r e. ( Base ` Q ) /\ s e. ( Base ` Q ) ) ) -> ( J ` ( r ( +g ` Q ) s ) ) = ( ( J ` r ) ( +g ` H ) ( J ` s ) ) )
98 6 7 8 9 14 17 53 97 isghmd 
 |-  ( ph -> J e. ( Q GrpHom H ) )