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 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
zndvdchrrhm.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
zndvdchrrhm.3 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) ∈ ℤ )
zndvdchrrhm.4 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) ∥ 𝑁 )
zndvdchrrhm.5 ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
zndvdchrrhm.6 ⊢ 𝐹 = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) )
Assertion zndvdchrrhm ( 𝜑 → 𝐹 ∈ ( 𝑍 RingHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 zndvdchrrhm.1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
2 zndvdchrrhm.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 zndvdchrrhm.3 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) ∈ ℤ )
4 zndvdchrrhm.4 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) ∥ 𝑁 )
5 zndvdchrrhm.5 ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
6 zndvdchrrhm.6 ⊢ 𝐹 = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) )
7 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8 eqid ⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
9 eqid ⊢ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
10 8 9 5 znbas2 ⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( Base ‘ 𝑍 ) )
11 7 10 syl ⊢ ( 𝜑 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( Base ‘ 𝑍 ) )
12 11 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) = ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) )
13 12 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) ) )
14 6 13 eqtrid ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) ) )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
17 16 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
18 1 17 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
19 eqid ⊢ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) = ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } )
20 nfcv ⊢ Ⅎ 𝑦 ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 )
21 nfcv ⊢ Ⅎ 𝑥 ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑦 )
22 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) = ( ( ℤRHom ‘ 𝑅 ) “ 𝑦 ) )
23 22 unieqd ⊢ ( 𝑥 = 𝑦 → ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) = ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑦 ) )
24 20 21 23 cbvmpt ⊢ ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑦 ) )
25 zringcrng ⊢ ℤring ∈ CRing
26 25 a1i ⊢ ( 𝜑 → ℤring ∈ CRing )
27 zringring ⊢ ℤring ∈ Ring
28 27 a1i ⊢ ( 𝜑 → ℤring ∈ Ring )
29 eqid ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
30 29 15 kerlidl ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) ∈ ( LIdeal ‘ ℤring ) )
31 18 30 syl ⊢ ( 𝜑 → ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) ∈ ( LIdeal ‘ ℤring ) )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑎 ∈ { 𝑁 } )
33 elsng ⊢ ( 𝑎 ∈ { 𝑁 } → ( 𝑎 ∈ { 𝑁 } ↔ 𝑎 = 𝑁 ) )
34 32 33 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → ( 𝑎 ∈ { 𝑁 } → 𝑎 = 𝑁 ) )
35 34 imp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) ∧ 𝑎 ∈ { 𝑁 } ) → 𝑎 = 𝑁 )
36 32 35 mpdan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑎 = 𝑁 )
37 zringbas ⊢ ℤ = ( Base ‘ ℤring )
38 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
39 37 38 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
40 17 39 syl ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
41 1 40 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
42 41 ffnd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
43 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
44 eqid ⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
45 44 16 15 chrdvds ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ 𝑁 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) )
46 1 43 45 syl2anc ⊢ ( 𝜑 → ( ( chr ‘ 𝑅 ) ∥ 𝑁 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) )
47 4 46 mpbid ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) )
48 fvexd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) ∈ V )
49 elsng ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) ∈ V → ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) )
50 48 49 syl ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) )
51 47 50 mpbird ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑁 ) ∈ { ( 0g ‘ 𝑅 ) } )
52 42 43 51 elpreimad ⊢ ( 𝜑 → 𝑁 ∈ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑁 ∈ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
54 36 53 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑎 ∈ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
55 54 ex ⊢ ( 𝜑 → ( 𝑎 ∈ { 𝑁 } → 𝑎 ∈ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) ) )
56 55 ssrdv ⊢ ( 𝜑 → { 𝑁 } ⊆ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
57 8 29 rspssp ⊢ ( ( ℤring ∈ Ring ∧ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) ∈ ( LIdeal ‘ ℤring ) ∧ { 𝑁 } ⊆ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
58 28 31 56 57 syl3anc ⊢ ( 𝜑 → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ( ◡ ( ℤRHom ‘ 𝑅 ) “ { ( 0g ‘ 𝑅 ) } ) )
59 26 crngringd ⊢ ( 𝜑 → ℤring ∈ Ring )
60 43 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑁 ∈ ℤ )
61 36 60 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑁 } ) → 𝑎 ∈ ℤ )
62 61 ex ⊢ ( 𝜑 → ( 𝑎 ∈ { 𝑁 } → 𝑎 ∈ ℤ ) )
63 62 ssrdv ⊢ ( 𝜑 → { 𝑁 } ⊆ ℤ )
64 8 37 29 rspcl ⊢ ( ( ℤring ∈ Ring ∧ { 𝑁 } ⊆ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
65 59 63 64 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
66 15 18 19 9 24 26 58 65 rhmqusnsg ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↦ ∪ ( ( ℤRHom ‘ 𝑅 ) “ 𝑥 ) ) ∈ ( ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) RingHom 𝑅 ) )
67 14 66 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) RingHom 𝑅 ) )
68 eqidd ⊢ ( 𝜑 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) )
69 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
70 8 9 5 znadd ⊢ ( 𝑁 ∈ ℕ0 → ( +g ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( +g ‘ 𝑍 ) )
71 7 70 syl ⊢ ( 𝜑 → ( +g ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( +g ‘ 𝑍 ) )
72 71 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ) ) → ( 𝑎 ( +g ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑍 ) 𝑏 ) )
73 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) )
74 8 9 5 znmul ⊢ ( 𝑁 ∈ ℕ0 → ( .r ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( .r ‘ 𝑍 ) )
75 7 74 syl ⊢ ( 𝜑 → ( .r ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( .r ‘ 𝑍 ) )
76 75 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ) ) → ( 𝑎 ( .r ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑍 ) 𝑏 ) )
77 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
78 68 69 11 69 72 73 76 77 rhmpropd ⊢ ( 𝜑 → ( ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) RingHom 𝑅 ) = ( 𝑍 RingHom 𝑅 ) )
79 67 78 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 RingHom 𝑅 ) )