Metamath Proof Explorer

Theorem zndvdchrrhm

Description: Construction of a ring homomorphism from Z/nZ to R when the characteristic of R divides N . (Contributed by metakunt, 4-Jun-2025)

Ref Expression
Hypotheses zndvdchrrhm.1 
|- ( ph -> R e. Ring )
zndvdchrrhm.2 
|- ( ph -> N e. NN )
zndvdchrrhm.3 
|- ( ph -> ( chr ` R ) e. ZZ )
zndvdchrrhm.4 
|- ( ph -> ( chr ` R ) || N )
zndvdchrrhm.5 
|- Z = ( Z/nZ ` N )
zndvdchrrhm.6 
|- F = ( x e. ( Base ` Z ) |-> U. ( ( ZRHom ` R ) " x ) )
Assertion zndvdchrrhm 
|- ( ph -> F e. ( Z RingHom R ) )

Proof

Step Hyp Ref Expression
1 zndvdchrrhm.1 
 |-  ( ph -> R e. Ring )
2 zndvdchrrhm.2 
 |-  ( ph -> N e. NN )
3 zndvdchrrhm.3 
 |-  ( ph -> ( chr ` R ) e. ZZ )
4 zndvdchrrhm.4 
 |-  ( ph -> ( chr ` R ) || N )
5 zndvdchrrhm.5 
 |-  Z = ( Z/nZ ` N )
6 zndvdchrrhm.6 
 |-  F = ( x e. ( Base ` Z ) |-> U. ( ( ZRHom ` R ) " x ) )
7 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
8 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
9 eqid 
 |-  ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
10 8 9 5 znbas2 
 |-  ( N e. NN0 -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( Base ` Z ) )
11 7 10 syl 
 |-  ( ph -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( Base ` Z ) )
12 11 eqcomd 
 |-  ( ph -> ( Base ` Z ) = ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) )
13 12 mpteq1d 
 |-  ( ph -> ( x e. ( Base ` Z ) |-> U. ( ( ZRHom ` R ) " x ) ) = ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |-> U. ( ( ZRHom ` R ) " x ) ) )
14 6 13 eqtrid 
 |-  ( ph -> F = ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |-> U. ( ( ZRHom ` R ) " x ) ) )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
17 16 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
18 1 17 syl 
 |-  ( ph -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
19 eqid 
 |-  ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) = ( `' ( ZRHom ` R ) " { ( 0g ` R ) } )
20 nfcv 
 |-  F/_ y U. ( ( ZRHom ` R ) " x )
21 nfcv 
 |-  F/_ x U. ( ( ZRHom ` R ) " y )
22 imaeq2 
 |-  ( x = y -> ( ( ZRHom ` R ) " x ) = ( ( ZRHom ` R ) " y ) )
23 22 unieqd 
 |-  ( x = y -> U. ( ( ZRHom ` R ) " x ) = U. ( ( ZRHom ` R ) " y ) )
24 20 21 23 cbvmpt 
 |-  ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |-> U. ( ( ZRHom ` R ) " x ) ) = ( y e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |-> U. ( ( ZRHom ` R ) " y ) )
25 zringcrng 
 |-  ZZring e. CRing
26 25 a1i 
 |-  ( ph -> ZZring e. CRing )
27 zringring 
 |-  ZZring e. Ring
28 27 a1i 
 |-  ( ph -> ZZring e. Ring )
29 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
30 29 15 kerlidl 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) e. ( LIdeal ` ZZring ) )
31 18 30 syl 
 |-  ( ph -> ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) e. ( LIdeal ` ZZring ) )
32 simpr 
 |-  ( ( ph /\ a e. { N } ) -> a e. { N } )
33 elsng 
 |-  ( a e. { N } -> ( a e. { N } <-> a = N ) )
34 32 33 syl5ibcom 
 |-  ( ( ph /\ a e. { N } ) -> ( a e. { N } -> a = N ) )
35 34 imp 
 |-  ( ( ( ph /\ a e. { N } ) /\ a e. { N } ) -> a = N )
36 32 35 mpdan 
 |-  ( ( ph /\ a e. { N } ) -> a = N )
37 zringbas 
 |-  ZZ = ( Base ` ZZring )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 37 38 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
40 17 39 syl 
 |-  ( R e. Ring -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
41 1 40 syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
42 41 ffnd 
 |-  ( ph -> ( ZRHom ` R ) Fn ZZ )
43 2 nnzd 
 |-  ( ph -> N e. ZZ )
44 eqid 
 |-  ( chr ` R ) = ( chr ` R )
45 44 16 15 chrdvds 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( ( chr ` R ) || N <-> ( ( ZRHom ` R ) ` N ) = ( 0g ` R ) ) )
46 1 43 45 syl2anc 
 |-  ( ph -> ( ( chr ` R ) || N <-> ( ( ZRHom ` R ) ` N ) = ( 0g ` R ) ) )
47 4 46 mpbid 
 |-  ( ph -> ( ( ZRHom ` R ) ` N ) = ( 0g ` R ) )
48 fvexd 
 |-  ( ph -> ( ( ZRHom ` R ) ` N ) e. _V )
49 elsng 
 |-  ( ( ( ZRHom ` R ) ` N ) e. _V -> ( ( ( ZRHom ` R ) ` N ) e. { ( 0g ` R ) } <-> ( ( ZRHom ` R ) ` N ) = ( 0g ` R ) ) )
50 48 49 syl 
 |-  ( ph -> ( ( ( ZRHom ` R ) ` N ) e. { ( 0g ` R ) } <-> ( ( ZRHom ` R ) ` N ) = ( 0g ` R ) ) )
51 47 50 mpbird 
 |-  ( ph -> ( ( ZRHom ` R ) ` N ) e. { ( 0g ` R ) } )
52 42 43 51 elpreimad 
 |-  ( ph -> N e. ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
53 52 adantr 
 |-  ( ( ph /\ a e. { N } ) -> N e. ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
54 36 53 eqeltrd 
 |-  ( ( ph /\ a e. { N } ) -> a e. ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
55 54 ex 
 |-  ( ph -> ( a e. { N } -> a e. ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) ) )
56 55 ssrdv 
 |-  ( ph -> { N } C_ ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
57 8 29 rspssp 
 |-  ( ( ZZring e. Ring /\ ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) e. ( LIdeal ` ZZring ) /\ { N } C_ ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) ) -> ( ( RSpan ` ZZring ) ` { N } ) C_ ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
58 28 31 56 57 syl3anc 
 |-  ( ph -> ( ( RSpan ` ZZring ) ` { N } ) C_ ( `' ( ZRHom ` R ) " { ( 0g ` R ) } ) )
59 26 crngringd 
 |-  ( ph -> ZZring e. Ring )
60 43 adantr 
 |-  ( ( ph /\ a e. { N } ) -> N e. ZZ )
61 36 60 eqeltrd 
 |-  ( ( ph /\ a e. { N } ) -> a e. ZZ )
62 61 ex 
 |-  ( ph -> ( a e. { N } -> a e. ZZ ) )
63 62 ssrdv 
 |-  ( ph -> { N } C_ ZZ )
64 8 37 29 rspcl 
 |-  ( ( ZZring e. Ring /\ { N } C_ ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) )
65 59 63 64 syl2anc 
 |-  ( ph -> ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) )
66 15 18 19 9 24 26 58 65 rhmqusnsg 
 |-  ( ph -> ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |-> U. ( ( ZRHom ` R ) " x ) ) e. ( ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) RingHom R ) )
67 14 66 eqeltrd 
 |-  ( ph -> F e. ( ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) RingHom R ) )
68 eqidd 
 |-  ( ph -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) )
69 eqidd 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
70 8 9 5 znadd 
 |-  ( N e. NN0 -> ( +g ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( +g ` Z ) )
71 7 70 syl 
 |-  ( ph -> ( +g ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( +g ` Z ) )
72 71 oveqdr 
 |-  ( ( ph /\ ( a e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) /\ b e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) ) ) -> ( a ( +g ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) b ) = ( a ( +g ` Z ) b ) )
73 eqidd 
 |-  ( ( ph /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( a ( +g ` R ) b ) = ( a ( +g ` R ) b ) )
74 8 9 5 znmul 
 |-  ( N e. NN0 -> ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( .r ` Z ) )
75 7 74 syl 
 |-  ( ph -> ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( .r ` Z ) )
76 75 oveqdr 
 |-  ( ( ph /\ ( a e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) /\ b e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) ) ) -> ( a ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) b ) = ( a ( .r ` Z ) b ) )
77 eqidd 
 |-  ( ( ph /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( a ( .r ` R ) b ) = ( a ( .r ` R ) b ) )
78 68 69 11 69 72 73 76 77 rhmpropd 
 |-  ( ph -> ( ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) RingHom R ) = ( Z RingHom R ) )
79 67 78 eleqtrd 
 |-  ( ph -> F e. ( Z RingHom R ) )