Metamath Proof Explorer

Theorem rhmqusspan

Description: Ring homomorphism out of a quotient given an ideal spanned by a singleton. (Contributed by metakunt, 7-Jun-2025)

Ref Expression
Hypotheses rhmqusspan.1 
|- .0. = ( 0g ` H )
rhmqusspan.2 
|- ( ph -> F e. ( G RingHom H ) )
rhmqusspan.3 
|- K = ( `' F " { .0. } )
rhmqusspan.4 
|- Q = ( G /s ( G ~QG N ) )
rhmqusspan.5 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
rhmqusspan.6 
|- ( ph -> G e. CRing )
rhmqusspan.7 
|- N = ( ( RSpan ` G ) ` { X } )
rhmqusspan.8 
|- ( ph -> X e. ( Base ` G ) )
rhmqusspan.9 
|- ( ph -> ( F ` X ) = .0. )
Assertion rhmqusspan 
|- ( ph -> ( J e. ( Q RingHom H ) /\ A. g e. ( Base ` G ) ( J ` [ g ] ( G ~QG N ) ) = ( F ` g ) ) )

Proof

Step Hyp Ref Expression
1 rhmqusspan.1 
 |-  .0. = ( 0g ` H )
2 rhmqusspan.2 
 |-  ( ph -> F e. ( G RingHom H ) )
3 rhmqusspan.3 
 |-  K = ( `' F " { .0. } )
4 rhmqusspan.4 
 |-  Q = ( G /s ( G ~QG N ) )
5 rhmqusspan.5 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
6 rhmqusspan.6 
 |-  ( ph -> G e. CRing )
7 rhmqusspan.7 
 |-  N = ( ( RSpan ` G ) ` { X } )
8 rhmqusspan.8 
 |-  ( ph -> X e. ( Base ` G ) )
9 rhmqusspan.9 
 |-  ( ph -> ( F ` X ) = .0. )
10 6 crngringd 
 |-  ( ph -> G e. Ring )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 eqid 
 |-  ( RSpan ` G ) = ( RSpan ` G )
13 eqid 
 |-  ( ||r ` G ) = ( ||r ` G )
14 11 12 13 rspsn 
 |-  ( ( G e. Ring /\ X e. ( Base ` G ) ) -> ( ( RSpan ` G ) ` { X } ) = { y | X ( ||r ` G ) y } )
15 10 8 14 syl2anc 
 |-  ( ph -> ( ( RSpan ` G ) ` { X } ) = { y | X ( ||r ` G ) y } )
16 15 eleq2d 
 |-  ( ph -> ( x e. ( ( RSpan ` G ) ` { X } ) <-> x e. { y | X ( ||r ` G ) y } ) )
17 16 biimpd 
 |-  ( ph -> ( x e. ( ( RSpan ` G ) ` { X } ) -> x e. { y | X ( ||r ` G ) y } ) )
18 17 imp 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> x e. { y | X ( ||r ` G ) y } )
19 vex 
 |-  x e. _V
20 19 a1i 
 |-  ( ph -> x e. _V )
21 breq2 
 |-  ( y = x -> ( X ( ||r ` G ) y <-> X ( ||r ` G ) x ) )
22 21 elabg 
 |-  ( x e. _V -> ( x e. { y | X ( ||r ` G ) y } <-> X ( ||r ` G ) x ) )
23 22 biimpd 
 |-  ( x e. _V -> ( x e. { y | X ( ||r ` G ) y } -> X ( ||r ` G ) x ) )
24 20 23 syl 
 |-  ( ph -> ( x e. { y | X ( ||r ` G ) y } -> X ( ||r ` G ) x ) )
25 24 imp 
 |-  ( ( ph /\ x e. { y | X ( ||r ` G ) y } ) -> X ( ||r ` G ) x )
26 eqid 
 |-  ( .r ` G ) = ( .r ` G )
27 11 13 26 dvdsr 
 |-  ( X ( ||r ` G ) x <-> ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) )
28 27 biimpi 
 |-  ( X ( ||r ` G ) x -> ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) )
29 28 adantl 
 |-  ( ( ph /\ X ( ||r ` G ) x ) -> ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) )
30 fveq2 
 |-  ( ( z ( .r ` G ) X ) = x -> ( F ` ( z ( .r ` G ) X ) ) = ( F ` x ) )
31 30 eqcomd 
 |-  ( ( z ( .r ` G ) X ) = x -> ( F ` x ) = ( F ` ( z ( .r ` G ) X ) ) )
32 31 adantl 
 |-  ( ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) /\ ( z ( .r ` G ) X ) = x ) -> ( F ` x ) = ( F ` ( z ( .r ` G ) X ) ) )
33 2 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> F e. ( G RingHom H ) )
34 simpr 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> z e. ( Base ` G ) )
35 8 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> X e. ( Base ` G ) )
36 eqid 
 |-  ( .r ` H ) = ( .r ` H )
37 11 26 36 rhmmul 
 |-  ( ( F e. ( G RingHom H ) /\ z e. ( Base ` G ) /\ X e. ( Base ` G ) ) -> ( F ` ( z ( .r ` G ) X ) ) = ( ( F ` z ) ( .r ` H ) ( F ` X ) ) )
38 33 34 35 37 syl3anc 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( F ` ( z ( .r ` G ) X ) ) = ( ( F ` z ) ( .r ` H ) ( F ` X ) ) )
39 9 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( F ` X ) = .0. )
40 39 oveq2d 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( ( F ` z ) ( .r ` H ) ( F ` X ) ) = ( ( F ` z ) ( .r ` H ) .0. ) )
41 rhmrcl2 
 |-  ( F e. ( G RingHom H ) -> H e. Ring )
42 ringsrg 
 |-  ( H e. Ring -> H e. SRing )
43 33 41 42 3syl 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> H e. SRing )
44 eqid 
 |-  ( Base ` H ) = ( Base ` H )
45 11 44 rhmf 
 |-  ( F e. ( G RingHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
46 2 45 syl 
 |-  ( ph -> F : ( Base ` G ) --> ( Base ` H ) )
47 46 adantr 
 |-  ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) -> F : ( Base ` G ) --> ( Base ` H ) )
48 47 ffvelcdmda 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( F ` z ) e. ( Base ` H ) )
49 44 36 1 srgrz 
 |-  ( ( H e. SRing /\ ( F ` z ) e. ( Base ` H ) ) -> ( ( F ` z ) ( .r ` H ) .0. ) = .0. )
50 43 48 49 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( ( F ` z ) ( .r ` H ) .0. ) = .0. )
51 40 50 eqtrd 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( ( F ` z ) ( .r ` H ) ( F ` X ) ) = .0. )
52 38 51 eqtrd 
 |-  ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) -> ( F ` ( z ( .r ` G ) X ) ) = .0. )
53 52 adantr 
 |-  ( ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) /\ ( z ( .r ` G ) X ) = x ) -> ( F ` ( z ( .r ` G ) X ) ) = .0. )
54 32 53 eqtrd 
 |-  ( ( ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) /\ z e. ( Base ` G ) ) /\ ( z ( .r ` G ) X ) = x ) -> ( F ` x ) = .0. )
55 nfv 
 |-  F/ z ( y ( .r ` G ) X ) = x
56 nfv 
 |-  F/ y ( z ( .r ` G ) X ) = x
57 oveq1 
 |-  ( y = z -> ( y ( .r ` G ) X ) = ( z ( .r ` G ) X ) )
58 57 eqeq1d 
 |-  ( y = z -> ( ( y ( .r ` G ) X ) = x <-> ( z ( .r ` G ) X ) = x ) )
59 55 56 58 cbvrexw 
 |-  ( E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x <-> E. z e. ( Base ` G ) ( z ( .r ` G ) X ) = x )
60 59 biimpi 
 |-  ( E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x -> E. z e. ( Base ` G ) ( z ( .r ` G ) X ) = x )
61 60 adantl 
 |-  ( ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) -> E. z e. ( Base ` G ) ( z ( .r ` G ) X ) = x )
62 61 adantl 
 |-  ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) -> E. z e. ( Base ` G ) ( z ( .r ` G ) X ) = x )
63 54 62 r19.29a 
 |-  ( ( ph /\ ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) ) -> ( F ` x ) = .0. )
64 63 ex 
 |-  ( ph -> ( ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) -> ( F ` x ) = .0. ) )
65 64 adantr 
 |-  ( ( ph /\ X ( ||r ` G ) x ) -> ( ( X e. ( Base ` G ) /\ E. y e. ( Base ` G ) ( y ( .r ` G ) X ) = x ) -> ( F ` x ) = .0. ) )
66 29 65 mpd 
 |-  ( ( ph /\ X ( ||r ` G ) x ) -> ( F ` x ) = .0. )
67 66 ex 
 |-  ( ph -> ( X ( ||r ` G ) x -> ( F ` x ) = .0. ) )
68 67 adantr 
 |-  ( ( ph /\ x e. { y | X ( ||r ` G ) y } ) -> ( X ( ||r ` G ) x -> ( F ` x ) = .0. ) )
69 25 68 mpd 
 |-  ( ( ph /\ x e. { y | X ( ||r ` G ) y } ) -> ( F ` x ) = .0. )
70 69 ex 
 |-  ( ph -> ( x e. { y | X ( ||r ` G ) y } -> ( F ` x ) = .0. ) )
71 70 adantr 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( x e. { y | X ( ||r ` G ) y } -> ( F ` x ) = .0. ) )
72 18 71 mpd 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( F ` x ) = .0. )
73 fvexd 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( F ` x ) e. _V )
74 elsng 
 |-  ( ( F ` x ) e. _V -> ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. ) )
75 73 74 syl 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. ) )
76 72 75 mpbird 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( F ` x ) e. { .0. } )
77 46 ffund 
 |-  ( ph -> Fun F )
78 77 adantr 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> Fun F )
79 eqid 
 |-  ( LIdeal ` G ) = ( LIdeal ` G )
80 79 11 lidl1 
 |-  ( G e. Ring -> ( Base ` G ) e. ( LIdeal ` G ) )
81 10 80 syl 
 |-  ( ph -> ( Base ` G ) e. ( LIdeal ` G ) )
82 8 snssd 
 |-  ( ph -> { X } C_ ( Base ` G ) )
83 12 79 rspssp 
 |-  ( ( G e. Ring /\ ( Base ` G ) e. ( LIdeal ` G ) /\ { X } C_ ( Base ` G ) ) -> ( ( RSpan ` G ) ` { X } ) C_ ( Base ` G ) )
84 10 81 82 83 syl3anc 
 |-  ( ph -> ( ( RSpan ` G ) ` { X } ) C_ ( Base ` G ) )
85 84 sselda 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> x e. ( Base ` G ) )
86 fdm 
 |-  ( F : ( Base ` G ) --> ( Base ` H ) -> dom F = ( Base ` G ) )
87 46 86 syl 
 |-  ( ph -> dom F = ( Base ` G ) )
88 87 adantr 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> dom F = ( Base ` G ) )
89 85 88 eleqtrrd 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> x e. dom F )
90 fvimacnv 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) e. { .0. } <-> x e. ( `' F " { .0. } ) ) )
91 78 89 90 syl2anc 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> ( ( F ` x ) e. { .0. } <-> x e. ( `' F " { .0. } ) ) )
92 76 91 mpbid 
 |-  ( ( ph /\ x e. ( ( RSpan ` G ) ` { X } ) ) -> x e. ( `' F " { .0. } ) )
93 92 ex 
 |-  ( ph -> ( x e. ( ( RSpan ` G ) ` { X } ) -> x e. ( `' F " { .0. } ) ) )
94 93 ssrdv 
 |-  ( ph -> ( ( RSpan ` G ) ` { X } ) C_ ( `' F " { .0. } ) )
95 3 eqcomi 
 |-  ( `' F " { .0. } ) = K
96 94 95 sseqtrdi 
 |-  ( ph -> ( ( RSpan ` G ) ` { X } ) C_ K )
97 7 96 eqsstrid 
 |-  ( ph -> N C_ K )
98 12 11 79 rspcl 
 |-  ( ( G e. Ring /\ { X } C_ ( Base ` G ) ) -> ( ( RSpan ` G ) ` { X } ) e. ( LIdeal ` G ) )
99 10 82 98 syl2anc 
 |-  ( ph -> ( ( RSpan ` G ) ` { X } ) e. ( LIdeal ` G ) )
100 7 99 eqeltrid 
 |-  ( ph -> N e. ( LIdeal ` G ) )
101 1 2 3 4 5 6 97 100 rhmqusnsg 
 |-  ( ph -> J e. ( Q RingHom H ) )
102 2 adantr 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> F e. ( G RingHom H ) )
103 rhmghm 
 |-  ( F e. ( G RingHom H ) -> F e. ( G GrpHom H ) )
104 102 103 syl 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> F e. ( G GrpHom H ) )
105 97 adantr 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> N C_ K )
106 lidlnsg 
 |-  ( ( G e. Ring /\ N e. ( LIdeal ` G ) ) -> N e. ( NrmSGrp ` G ) )
107 10 100 106 syl2anc 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
108 107 adantr 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> N e. ( NrmSGrp ` G ) )
109 simpr 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> g e. ( Base ` G ) )
110 1 104 3 4 5 105 108 109 ghmqusnsglem1 
 |-  ( ( ph /\ g e. ( Base ` G ) ) -> ( J ` [ g ] ( G ~QG N ) ) = ( F ` g ) )
111 110 ralrimiva 
 |-  ( ph -> A. g e. ( Base ` G ) ( J ` [ g ] ( G ~QG N ) ) = ( F ` g ) )
112 101 111 jca 
 |-  ( ph -> ( J e. ( Q RingHom H ) /\ A. g e. ( Base ` G ) ( J ` [ g ] ( G ~QG N ) ) = ( F ` g ) ) )