Metamath Proof Explorer

Theorem rhmqusnsg

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

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

Proof

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