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 ⊢ φ → R ∈ Ring
zndvdchrrhm.2 ⊢ φ → N ∈ ℕ
zndvdchrrhm.3 ⊢ φ → chr ⁡ R ∈ ℤ
zndvdchrrhm.4 ⊢ φ → chr ⁡ R ∥ N
zndvdchrrhm.5 ⊢ Z = ℤ/Nℤ
zndvdchrrhm.6 ⊢ F = x ∈ Base Z ⟼ ⋃ ℤRHom ⁡ R x
Assertion zndvdchrrhm ⊢ φ → F ∈ Z RingHom R

Proof

Step Hyp Ref Expression
1 zndvdchrrhm.1 ⊢ φ → R ∈ Ring
2 zndvdchrrhm.2 ⊢ φ → N ∈ ℕ
3 zndvdchrrhm.3 ⊢ φ → chr ⁡ R ∈ ℤ
4 zndvdchrrhm.4 ⊢ φ → chr ⁡ R ∥ N
5 zndvdchrrhm.5 ⊢ Z = ℤ/Nℤ
6 zndvdchrrhm.6 ⊢ F = x ∈ Base Z ⟼ ⋃ ℤRHom ⁡ R x
7 2 nnnn0d ⊢ φ → N ∈ ℕ 0
8 eqid ⊢ RSpan ⁡ ℤ ring = RSpan ⁡ ℤ ring
9 eqid ⊢ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N
10 8 9 5 znbas2 ⊢ N ∈ ℕ 0 → Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = Base Z
11 7 10 syl ⊢ φ → Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = Base Z
12 11 eqcomd ⊢ φ → Base Z = Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N
13 12 mpteq1d ⊢ φ → x ∈ Base Z ⟼ ⋃ ℤRHom ⁡ R x = x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ⟼ ⋃ ℤRHom ⁡ R x
14 6 13 eqtrid ⊢ φ → F = x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ⟼ ⋃ ℤRHom ⁡ R x
15 eqid ⊢ 0 R = 0 R
16 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
17 16 zrhrhm ⊢ R ∈ Ring → ℤRHom ⁡ R ∈ ℤ ring RingHom R
18 1 17 syl ⊢ φ → ℤRHom ⁡ R ∈ ℤ ring RingHom R
19 eqid ⊢ ℤRHom ⁡ R -1 0 R = ℤRHom ⁡ R -1 0 R
20 nfcv ⊢ Ⅎ _ y ⋃ ℤRHom ⁡ R x
21 nfcv ⊢ Ⅎ _ x ⋃ ℤRHom ⁡ R y
22 imaeq2 ⊢ x = y → ℤRHom ⁡ R x = ℤRHom ⁡ R y
23 22 unieqd ⊢ x = y → ⋃ ℤRHom ⁡ R x = ⋃ ℤRHom ⁡ R y
24 20 21 23 cbvmpt ⊢ x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ⟼ ⋃ ℤRHom ⁡ R x = y ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ⟼ ⋃ ℤRHom ⁡ R y
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 ⁡ R ∈ ℤ ring RingHom R → ℤRHom ⁡ R -1 0 R ∈ LIdeal ⁡ ℤ ring
31 18 30 syl ⊢ φ → ℤRHom ⁡ R -1 0 R ∈ LIdeal ⁡ ℤ ring
32 simpr ⊢ φ ∧ a ∈ N → a ∈ N
33 elsng ⊢ a ∈ N → a ∈ N ↔ a = N
34 32 33 syl5ibcom ⊢ φ ∧ a ∈ N → a ∈ N → a = N
35 34 imp ⊢ φ ∧ a ∈ N ∧ a ∈ N → a = N
36 32 35 mpdan ⊢ φ ∧ a ∈ N → a = N
37 zringbas ⊢ ℤ = Base ℤ ring
38 eqid ⊢ Base R = Base R
39 37 38 rhmf ⊢ ℤRHom ⁡ R ∈ ℤ ring RingHom R → ℤRHom ⁡ R : ℤ ⟶ Base R
40 17 39 syl ⊢ R ∈ Ring → ℤRHom ⁡ R : ℤ ⟶ Base R
41 1 40 syl ⊢ φ → ℤRHom ⁡ R : ℤ ⟶ Base R
42 41 ffnd ⊢ φ → ℤRHom ⁡ R Fn ℤ
43 2 nnzd ⊢ φ → N ∈ ℤ
44 eqid ⊢ chr ⁡ R = chr ⁡ R
45 44 16 15 chrdvds ⊢ R ∈ Ring ∧ N ∈ ℤ → chr ⁡ R ∥ N ↔ ℤRHom ⁡ R ⁡ N = 0 R
46 1 43 45 syl2anc ⊢ φ → chr ⁡ R ∥ N ↔ ℤRHom ⁡ R ⁡ N = 0 R
47 4 46 mpbid ⊢ φ → ℤRHom ⁡ R ⁡ N = 0 R
48 fvexd ⊢ φ → ℤRHom ⁡ R ⁡ N ∈ V
49 elsng ⊢ ℤRHom ⁡ R ⁡ N ∈ V → ℤRHom ⁡ R ⁡ N ∈ 0 R ↔ ℤRHom ⁡ R ⁡ N = 0 R
50 48 49 syl ⊢ φ → ℤRHom ⁡ R ⁡ N ∈ 0 R ↔ ℤRHom ⁡ R ⁡ N = 0 R
51 47 50 mpbird ⊢ φ → ℤRHom ⁡ R ⁡ N ∈ 0 R
52 42 43 51 elpreimad ⊢ φ → N ∈ ℤRHom ⁡ R -1 0 R
53 52 adantr ⊢ φ ∧ a ∈ N → N ∈ ℤRHom ⁡ R -1 0 R
54 36 53 eqeltrd ⊢ φ ∧ a ∈ N → a ∈ ℤRHom ⁡ R -1 0 R
55 54 ex ⊢ φ → a ∈ N → a ∈ ℤRHom ⁡ R -1 0 R
56 55 ssrdv ⊢ φ → N ⊆ ℤRHom ⁡ R -1 0 R
57 8 29 rspssp ⊢ ℤ ring ∈ Ring ∧ ℤRHom ⁡ R -1 0 R ∈ LIdeal ⁡ ℤ ring ∧ N ⊆ ℤRHom ⁡ R -1 0 R → RSpan ⁡ ℤ ring ⁡ N ⊆ ℤRHom ⁡ R -1 0 R
58 28 31 56 57 syl3anc ⊢ φ → RSpan ⁡ ℤ ring ⁡ N ⊆ ℤRHom ⁡ R -1 0 R
59 26 crngringd ⊢ φ → ℤ ring ∈ Ring
60 43 adantr ⊢ φ ∧ a ∈ N → N ∈ ℤ
61 36 60 eqeltrd ⊢ φ ∧ a ∈ N → a ∈ ℤ
62 61 ex ⊢ φ → a ∈ N → a ∈ ℤ
63 62 ssrdv ⊢ φ → N ⊆ ℤ
64 8 37 29 rspcl ⊢ ℤ ring ∈ Ring ∧ N ⊆ ℤ → RSpan ⁡ ℤ ring ⁡ N ∈ LIdeal ⁡ ℤ ring
65 59 63 64 syl2anc ⊢ φ → RSpan ⁡ ℤ ring ⁡ N ∈ LIdeal ⁡ ℤ ring
66 15 18 19 9 24 26 58 65 rhmqusnsg ⊢ φ → x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ⟼ ⋃ ℤRHom ⁡ R x ∈ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N RingHom R
67 14 66 eqeltrd ⊢ φ → F ∈ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N RingHom R
68 eqidd ⊢ φ → Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N
69 eqidd ⊢ φ → Base R = Base R
70 8 9 5 znadd ⊢ N ∈ ℕ 0 → + ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = + Z
71 7 70 syl ⊢ φ → + ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = + Z
72 71 oveqdr ⊢ φ ∧ a ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∧ b ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N → a + ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N b = a + Z b
73 eqidd ⊢ φ ∧ a ∈ Base R ∧ b ∈ Base R → a + R b = a + R b
74 8 9 5 znmul ⊢ N ∈ ℕ 0 → ⋅ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = ⋅ Z
75 7 74 syl ⊢ φ → ⋅ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = ⋅ Z
76 75 oveqdr ⊢ φ ∧ a ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∧ b ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N → a ⋅ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N b = a ⋅ Z b
77 eqidd ⊢ φ ∧ a ∈ Base R ∧ b ∈ Base R → a ⋅ R b = a ⋅ R b
78 68 69 11 69 72 73 76 77 rhmpropd ⊢ φ → ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N RingHom R = Z RingHom R
79 67 78 eleqtrd ⊢ φ → F ∈ Z RingHom R