Metamath Proof Explorer

Theorem rhmquskerlem

Description: The mapping J induced by a ring homomorphism F from the quotient group Q over F 's kernel K is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 rhmqusker.1 
 |-  .0. = ( 0g ` H )
2 rhmqusker.f 
 |-  ( ph -> F e. ( G RingHom H ) )
3 rhmqusker.k 
 |-  K = ( `' F " { .0. } )
4 rhmqusker.q 
 |-  Q = ( G /s ( G ~QG K ) )
5 rhmquskerlem.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
6 rhmquskerlem.2 
 |-  ( ph -> G e. CRing )
7 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
8 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
9 eqid 
 |-  ( 1r ` H ) = ( 1r ` H )
10 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
11 eqid 
 |-  ( .r ` H ) = ( .r ` H )
12 rhmrcl1 
 |-  ( F e. ( G RingHom H ) -> G e. Ring )
13 2 12 syl 
 |-  ( ph -> G e. Ring )
14 eqid 
 |-  ( LIdeal ` G ) = ( LIdeal ` G )
15 14 1 kerlidl 
 |-  ( F e. ( G RingHom H ) -> ( `' F " { .0. } ) e. ( LIdeal ` G ) )
16 2 15 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( LIdeal ` G ) )
17 3 16 eqeltrid 
 |-  ( ph -> K e. ( LIdeal ` G ) )
18 14 crng2idl 
 |-  ( G e. CRing -> ( LIdeal ` G ) = ( 2Ideal ` G ) )
19 6 18 syl 
 |-  ( ph -> ( LIdeal ` G ) = ( 2Ideal ` G ) )
20 17 19 eleqtrd 
 |-  ( ph -> K e. ( 2Ideal ` G ) )
21 eqid 
 |-  ( 2Ideal ` G ) = ( 2Ideal ` G )
22 eqid 
 |-  ( 1r ` G ) = ( 1r ` G )
23 4 21 22 qus1 
 |-  ( ( G e. Ring /\ K e. ( 2Ideal ` G ) ) -> ( Q e. Ring /\ [ ( 1r ` G ) ] ( G ~QG K ) = ( 1r ` Q ) ) )
24 13 20 23 syl2anc 
 |-  ( ph -> ( Q e. Ring /\ [ ( 1r ` G ) ] ( G ~QG K ) = ( 1r ` Q ) ) )
25 24 simpld 
 |-  ( ph -> Q e. Ring )
26 rhmrcl2 
 |-  ( F e. ( G RingHom H ) -> H e. Ring )
27 2 26 syl 
 |-  ( ph -> H e. Ring )
28 rhmghm 
 |-  ( F e. ( G RingHom H ) -> F e. ( G GrpHom H ) )
29 2 28 syl 
 |-  ( ph -> F e. ( G GrpHom H ) )
30 eqid 
 |-  ( Base ` G ) = ( Base ` G )
31 30 22 ringidcl 
 |-  ( G e. Ring -> ( 1r ` G ) e. ( Base ` G ) )
32 13 31 syl 
 |-  ( ph -> ( 1r ` G ) e. ( Base ` G ) )
33 1 29 3 4 5 32 ghmquskerlem1 
 |-  ( ph -> ( J ` [ ( 1r ` G ) ] ( G ~QG K ) ) = ( F ` ( 1r ` G ) ) )
34 24 simprd 
 |-  ( ph -> [ ( 1r ` G ) ] ( G ~QG K ) = ( 1r ` Q ) )
35 34 fveq2d 
 |-  ( ph -> ( J ` [ ( 1r ` G ) ] ( G ~QG K ) ) = ( J ` ( 1r ` Q ) ) )
36 22 9 rhm1 
 |-  ( F e. ( G RingHom H ) -> ( F ` ( 1r ` G ) ) = ( 1r ` H ) )
37 2 36 syl 
 |-  ( ph -> ( F ` ( 1r ` G ) ) = ( 1r ` H ) )
38 33 35 37 3eqtr3d 
 |-  ( ph -> ( J ` ( 1r ` Q ) ) = ( 1r ` H ) )
39 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 RingHom H ) )
40 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
41 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
42 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
43 40 41 42 6 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
44 1 ghmker 
 |-  ( F e. ( G GrpHom H ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
45 29 44 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
46 3 45 eqeltrid 
 |-  ( ph -> K e. ( NrmSGrp ` G ) )
47 nsgsubg 
 |-  ( K e. ( NrmSGrp ` G ) -> K e. ( SubGrp ` G ) )
48 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
49 30 48 eqger 
 |-  ( K e. ( SubGrp ` G ) -> ( G ~QG K ) Er ( Base ` G ) )
50 46 47 49 3syl 
 |-  ( ph -> ( G ~QG K ) Er ( Base ` G ) )
51 50 qsss 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) C_ ~P ( Base ` G ) )
52 43 51 eqsstrrd 
 |-  ( ph -> ( Base ` Q ) C_ ~P ( Base ` G ) )
53 52 sselda 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ~P ( Base ` G ) )
54 53 elpwid 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r C_ ( Base ` G ) )
55 54 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 ) )
56 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 )
57 55 56 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 ) )
58 52 sselda 
 |-  ( ( ph /\ s e. ( Base ` Q ) ) -> s e. ~P ( Base ` G ) )
59 58 elpwid 
 |-  ( ( ph /\ s e. ( Base ` Q ) ) -> s C_ ( Base ` G ) )
60 59 adantlr 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> s C_ ( Base ` G ) )
61 60 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 ) )
62 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 )
63 61 62 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 ) )
64 eqid 
 |-  ( .r ` G ) = ( .r ` G )
65 30 64 11 rhmmul 
 |-  ( ( F e. ( G RingHom H ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( F ` ( x ( .r ` G ) y ) ) = ( ( F ` x ) ( .r ` H ) ( F ` y ) ) )
66 39 57 63 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 ) ) -> ( F ` ( x ( .r ` G ) y ) ) = ( ( F ` x ) ( .r ` H ) ( F ` y ) ) )
67 50 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 ) )
68 simp-6r 
 |-  ( ( ( ( ( ( ( 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 ) )
69 43 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 ) )
70 68 69 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 ) ) )
71 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ r e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ x e. r ) -> r = [ x ] ( G ~QG K ) )
72 67 70 56 71 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 ) )
73 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 ) )
74 73 69 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 ) ) )
75 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ s e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ y e. s ) -> s = [ y ] ( G ~QG K ) )
76 67 74 62 75 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 ) )
77 72 76 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 ( .r ` Q ) s ) = ( [ x ] ( G ~QG K ) ( .r ` Q ) [ y ] ( G ~QG K ) ) )
78 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 ) ) -> G e. CRing )
79 17 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. ( LIdeal ` G ) )
80 4 30 64 10 78 79 57 63 qusmul 
 |-  ( ( ( ( ( ( ( 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 ) ( .r ` Q ) [ y ] ( G ~QG K ) ) = [ ( x ( .r ` G ) y ) ] ( G ~QG K ) )
81 77 80 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> [ ( x ( .r ` G ) y ) ] ( G ~QG K ) = ( r ( .r ` Q ) s ) )
82 81 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 ` [ ( x ( .r ` G ) y ) ] ( G ~QG K ) ) = ( J ` ( r ( .r ` Q ) s ) ) )
83 39 28 syl 
 |-  ( ( ( ( ( ( ( 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 ) )
84 39 12 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. Ring )
85 30 64 84 57 63 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ y e. s ) /\ ( J ` s ) = ( F ` y ) ) -> ( x ( .r ` G ) y ) e. ( Base ` G ) )
86 1 83 3 4 5 85 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 ( .r ` G ) y ) ] ( G ~QG K ) ) = ( F ` ( x ( .r ` G ) y ) ) )
87 82 86 eqtr3d 
 |-  ( ( ( ( ( ( ( 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 ( .r ` Q ) s ) ) = ( F ` ( x ( .r ` G ) y ) ) )
88 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 ) )
89 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 ) )
90 88 89 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 ) ( .r ` H ) ( J ` s ) ) = ( ( F ` x ) ( .r ` H ) ( F ` y ) ) )
91 66 87 90 3eqtr4d 
 |-  ( ( ( ( ( ( ( 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 ( .r ` Q ) s ) ) = ( ( J ` r ) ( .r ` H ) ( J ` s ) ) )
92 29 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F e. ( G GrpHom H ) )
93 simpllr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> s e. ( Base ` Q ) )
94 1 92 3 4 5 93 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 ) )
95 91 94 r19.29a 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` ( r ( .r ` Q ) s ) ) = ( ( J ` r ) ( .r ` H ) ( J ` s ) ) )
96 29 ad2antrr 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
97 simplr 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> r e. ( Base ` Q ) )
98 1 96 3 4 5 97 ghmquskerlem2 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> E. x e. r ( J ` r ) = ( F ` x ) )
99 95 98 r19.29a 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ s e. ( Base ` Q ) ) -> ( J ` ( r ( .r ` Q ) s ) ) = ( ( J ` r ) ( .r ` H ) ( J ` s ) ) )
100 99 anasss 
 |-  ( ( ph /\ ( r e. ( Base ` Q ) /\ s e. ( Base ` Q ) ) ) -> ( J ` ( r ( .r ` Q ) s ) ) = ( ( J ` r ) ( .r ` H ) ( J ` s ) ) )
101 1 29 3 4 5 ghmquskerlem3 
 |-  ( ph -> J e. ( Q GrpHom H ) )
102 7 8 9 10 11 25 27 38 100 101 isrhm2d 
 |-  ( ph -> J e. ( Q RingHom H ) )