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