Metamath Proof Explorer

Theorem lmhmqusker

Description: A surjective module homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses lmhmqusker.1 
|- .0. = ( 0g ` H )
lmhmqusker.f 
|- ( ph -> F e. ( G LMHom H ) )
lmhmqusker.k 
|- K = ( `' F " { .0. } )
lmhmqusker.q 
|- Q = ( G /s ( G ~QG K ) )
lmhmqusker.s 
|- ( ph -> ran F = ( Base ` H ) )
lmhmqusker.j 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
Assertion lmhmqusker 
|- ( ph -> J e. ( Q LMIso H ) )

Proof

Step Hyp Ref Expression
1 lmhmqusker.1 
 |-  .0. = ( 0g ` H )
2 lmhmqusker.f 
 |-  ( ph -> F e. ( G LMHom H ) )
3 lmhmqusker.k 
 |-  K = ( `' F " { .0. } )
4 lmhmqusker.q 
 |-  Q = ( G /s ( G ~QG K ) )
5 lmhmqusker.s 
 |-  ( ph -> ran F = ( Base ` H ) )
6 lmhmqusker.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
7 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
8 eqid 
 |-  ( .s ` Q ) = ( .s ` Q )
9 eqid 
 |-  ( .s ` H ) = ( .s ` H )
10 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
11 eqid 
 |-  ( Scalar ` H ) = ( Scalar ` H )
12 eqid 
 |-  ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 lmhmlmod1 
 |-  ( F e. ( G LMHom H ) -> G e. LMod )
15 2 14 syl 
 |-  ( ph -> G e. LMod )
16 eqid 
 |-  ( LSubSp ` G ) = ( LSubSp ` G )
17 3 1 16 lmhmkerlss 
 |-  ( F e. ( G LMHom H ) -> K e. ( LSubSp ` G ) )
18 2 17 syl 
 |-  ( ph -> K e. ( LSubSp ` G ) )
19 4 13 15 18 quslmod 
 |-  ( ph -> Q e. LMod )
20 lmhmlmod2 
 |-  ( F e. ( G LMHom H ) -> H e. LMod )
21 2 20 syl 
 |-  ( ph -> H e. LMod )
22 eqid 
 |-  ( Scalar ` G ) = ( Scalar ` G )
23 22 11 lmhmsca 
 |-  ( F e. ( G LMHom H ) -> ( Scalar ` H ) = ( Scalar ` G ) )
24 2 23 syl 
 |-  ( ph -> ( Scalar ` H ) = ( Scalar ` G ) )
25 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
26 13 a1i 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
27 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
28 25 26 27 15 22 quss 
 |-  ( ph -> ( Scalar ` G ) = ( Scalar ` Q ) )
29 24 28 eqtrd 
 |-  ( ph -> ( Scalar ` H ) = ( Scalar ` Q ) )
30 lmghm 
 |-  ( F e. ( G LMHom H ) -> F e. ( G GrpHom H ) )
31 2 30 syl 
 |-  ( ph -> F e. ( G GrpHom H ) )
32 1 31 3 4 6 5 ghmqusker 
 |-  ( ph -> J e. ( Q GrpIso H ) )
33 gimghm 
 |-  ( J e. ( Q GrpIso H ) -> J e. ( Q GrpHom H ) )
34 32 33 syl 
 |-  ( ph -> J e. ( Q GrpHom H ) )
35 1 ghmker 
 |-  ( F e. ( G GrpHom H ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
36 31 35 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
37 3 36 eqeltrid 
 |-  ( ph -> K e. ( NrmSGrp ` G ) )
38 nsgsubg 
 |-  ( K e. ( NrmSGrp ` G ) -> K e. ( SubGrp ` G ) )
39 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
40 13 39 eqger 
 |-  ( K e. ( SubGrp ` G ) -> ( G ~QG K ) Er ( Base ` G ) )
41 37 38 40 3syl 
 |-  ( ph -> ( G ~QG K ) Er ( Base ` G ) )
42 41 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( G ~QG K ) Er ( Base ` G ) )
43 simpllr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> r e. ( Base ` Q ) )
44 25 26 27 15 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
45 44 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
46 43 45 eleqtrrd 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> r e. ( ( Base ` G ) /. ( G ~QG K ) ) )
47 simplr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> x e. r )
48 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ r e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ x e. r ) -> r = [ x ] ( G ~QG K ) )
49 42 46 47 48 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> r = [ x ] ( G ~QG K ) )
50 49 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( k ( .s ` Q ) r ) = ( k ( .s ` Q ) [ x ] ( G ~QG K ) ) )
51 eqid 
 |-  ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` G ) )
52 eqid 
 |-  ( .s ` G ) = ( .s ` G )
53 15 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> G e. LMod )
54 18 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> K e. ( LSubSp ` G ) )
55 simp-4r 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> k e. ( Base ` ( Scalar ` Q ) ) )
56 28 fveq2d 
 |-  ( ph -> ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` Q ) ) )
57 56 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` Q ) ) )
58 55 57 eleqtrrd 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> k e. ( Base ` ( Scalar ` G ) ) )
59 41 qsss 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) C_ ~P ( Base ` G ) )
60 44 59 eqsstrrd 
 |-  ( ph -> ( Base ` Q ) C_ ~P ( Base ` G ) )
61 60 sselda 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ~P ( Base ` G ) )
62 61 elpwid 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r C_ ( Base ` G ) )
63 62 ad5ant13 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> r C_ ( Base ` G ) )
64 63 47 sseldd 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> x e. ( Base ` G ) )
65 13 39 51 52 53 54 58 4 8 64 qusvsval 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( k ( .s ` Q ) [ x ] ( G ~QG K ) ) = [ ( k ( .s ` G ) x ) ] ( G ~QG K ) )
66 50 65 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( k ( .s ` Q ) r ) = [ ( k ( .s ` G ) x ) ] ( G ~QG K ) )
67 66 fveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` ( k ( .s ` Q ) r ) ) = ( J ` [ ( k ( .s ` G ) x ) ] ( G ~QG K ) ) )
68 31 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F e. ( G GrpHom H ) )
69 13 22 52 51 lmodvscl 
 |-  ( ( G e. LMod /\ k e. ( Base ` ( Scalar ` G ) ) /\ x e. ( Base ` G ) ) -> ( k ( .s ` G ) x ) e. ( Base ` G ) )
70 53 58 64 69 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( k ( .s ` G ) x ) e. ( Base ` G ) )
71 1 68 3 4 6 70 ghmquskerlem1 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` [ ( k ( .s ` G ) x ) ] ( G ~QG K ) ) = ( F ` ( k ( .s ` G ) x ) ) )
72 2 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F e. ( G LMHom H ) )
73 22 51 13 52 9 lmhmlin 
 |-  ( ( F e. ( G LMHom H ) /\ k e. ( Base ` ( Scalar ` G ) ) /\ x e. ( Base ` G ) ) -> ( F ` ( k ( .s ` G ) x ) ) = ( k ( .s ` H ) ( F ` x ) ) )
74 72 58 64 73 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( F ` ( k ( .s ` G ) x ) ) = ( k ( .s ` H ) ( F ` x ) ) )
75 67 71 74 3eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` ( k ( .s ` Q ) r ) ) = ( k ( .s ` H ) ( F ` x ) ) )
76 simpr 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` r ) = ( F ` x ) )
77 76 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( k ( .s ` H ) ( J ` r ) ) = ( k ( .s ` H ) ( F ` x ) ) )
78 75 77 eqtr4d 
 |-  ( ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` ( k ( .s ` Q ) r ) ) = ( k ( .s ` H ) ( J ` r ) ) )
79 31 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
80 simpr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) -> r e. ( Base ` Q ) )
81 1 79 3 4 6 80 ghmquskerlem2 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) -> E. x e. r ( J ` r ) = ( F ` x ) )
82 78 81 r19.29a 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` Q ) ) ) /\ r e. ( Base ` Q ) ) -> ( J ` ( k ( .s ` Q ) r ) ) = ( k ( .s ` H ) ( J ` r ) ) )
83 82 anasss 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` Q ) ) /\ r e. ( Base ` Q ) ) ) -> ( J ` ( k ( .s ` Q ) r ) ) = ( k ( .s ` H ) ( J ` r ) ) )
84 7 8 9 10 11 12 19 21 29 34 83 islmhmd 
 |-  ( ph -> J e. ( Q LMHom H ) )
85 eqid 
 |-  ( Base ` H ) = ( Base ` H )
86 7 85 gimf1o 
 |-  ( J e. ( Q GrpIso H ) -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
87 32 86 syl 
 |-  ( ph -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
88 7 85 islmim 
 |-  ( J e. ( Q LMIso H ) <-> ( J e. ( Q LMHom H ) /\ J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) ) )
89 84 87 88 sylanbrc 
 |-  ( ph -> J e. ( Q LMIso H ) )