Metamath Proof Explorer

Theorem ghmqusnsg

Description: The mapping H induced by a surjective group homomorphism F from the quotient group Q over a normal subgroup N of 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, 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 ) )
Assertion ghmqusnsg 
|- ( ph -> J e. ( Q GrpHom H ) )

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