Step | Hyp | Ref
| Expression |
1 | | prmnn 12222 |
. . . 4
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
2 | | nnnn0 9233 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ0) |
4 | | zntos.y |
. . . 4
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
5 | 4 | zncrng 14090 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
6 | 3, 5 | syl 14 |
. 2
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ CRing) |
7 | | crngring 13468 |
. . . . 5
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
8 | 1, 2, 5, 7 | 4syl 18 |
. . . 4
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Ring) |
9 | | hash2 10857 |
. . . . . 6
⊢
(♯‘2o) = 2 |
10 | | prmuz2 12243 |
. . . . . . . 8
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
11 | | eluzle 9590 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℙ → 2 ≤
𝑁) |
13 | | eqid 2189 |
. . . . . . . . 9
⊢
(Base‘𝑌) =
(Base‘𝑌) |
14 | 4, 13 | znhash 14101 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(♯‘(Base‘𝑌)) = 𝑁) |
15 | 1, 14 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℙ →
(♯‘(Base‘𝑌)) = 𝑁) |
16 | 12, 15 | breqtrrd 4053 |
. . . . . 6
⊢ (𝑁 ∈ ℙ → 2 ≤
(♯‘(Base‘𝑌))) |
17 | 9, 16 | eqbrtrid 4060 |
. . . . 5
⊢ (𝑁 ∈ ℙ →
(♯‘2o) ≤ (♯‘(Base‘𝑌))) |
18 | | 2onn 6561 |
. . . . . . . 8
⊢
2o ∈ ω |
19 | | nnfi 6915 |
. . . . . . . 8
⊢
(2o ∈ ω → 2o ∈
Fin) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢
2o ∈ Fin |
21 | 4, 13 | znfi 14100 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(Base‘𝑌) ∈
Fin) |
22 | | fihashdom 10848 |
. . . . . . 7
⊢
((2o ∈ Fin ∧ (Base‘𝑌) ∈ Fin) →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
23 | 20, 21, 22 | sylancr 414 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
24 | 1, 23 | syl 14 |
. . . . 5
⊢ (𝑁 ∈ ℙ →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
25 | 17, 24 | mpbid 147 |
. . . 4
⊢ (𝑁 ∈ ℙ →
2o ≼ (Base‘𝑌)) |
26 | 13 | isnzr2 13644 |
. . . 4
⊢ (𝑌 ∈ NzRing ↔ (𝑌 ∈ Ring ∧ 2o
≼ (Base‘𝑌))) |
27 | 8, 25, 26 | sylanbrc 417 |
. . 3
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ NzRing) |
28 | | eqid 2189 |
. . . . . . . 8
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
29 | 4, 13, 28 | znzrhfo 14093 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) |
30 | 3, 29 | syl 14 |
. . . . . 6
⊢ (𝑁 ∈ ℙ →
(ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) |
31 | | foelrn 5783 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑥 ∈ (Base‘𝑌)) → ∃𝑧 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑧)) |
32 | | foelrn 5783 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌)) → ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) |
33 | 31, 32 | anim12dan 600 |
. . . . . 6
⊢
(((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌))) → (∃𝑧 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤))) |
34 | 30, 33 | sylan 283 |
. . . . 5
⊢ ((𝑁 ∈ ℙ ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌))) → (∃𝑧 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤))) |
35 | | reeanv 2660 |
. . . . . . 7
⊢
(∃𝑧 ∈
ℤ ∃𝑤 ∈
ℤ (𝑥 =
((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) ↔ (∃𝑧 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤))) |
36 | | euclemma 12258 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑁 ∥ (𝑧 · 𝑤) ↔ (𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤))) |
37 | 36 | 3expb 1206 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) → (𝑁 ∥ (𝑧 · 𝑤) ↔ (𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤))) |
38 | 8 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) → 𝑌 ∈ Ring) |
39 | 28 | zrhrhm 14068 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
41 | | simprl 529 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) → 𝑧 ∈
ℤ) |
42 | | simprr 531 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) → 𝑤 ∈
ℤ) |
43 | | zringbas 14042 |
. . . . . . . . . . . . . . 15
⊢ ℤ =
(Base‘ℤring) |
44 | | zringmulr 14045 |
. . . . . . . . . . . . . . 15
⊢ ·
= (.r‘ℤring) |
45 | | eqid 2189 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑌) = (.r‘𝑌) |
46 | 43, 44, 45 | rhmmul 13624 |
. . . . . . . . . . . . . 14
⊢
(((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) ∧ 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑧 · 𝑤)) = (((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤))) |
47 | 40, 41, 42, 46 | syl3anc 1249 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
((ℤRHom‘𝑌)‘(𝑧 · 𝑤)) = (((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤))) |
48 | 47 | eqeq1d 2198 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
(((ℤRHom‘𝑌)‘(𝑧 · 𝑤)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌))) |
49 | | zmulcl 9356 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑧 · 𝑤) ∈ ℤ) |
50 | | eqid 2189 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑌) = (0g‘𝑌) |
51 | 4, 28, 50 | zndvds0 14095 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑧 · 𝑤) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 · 𝑤)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑧 · 𝑤))) |
52 | 3, 49, 51 | syl2an 289 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
(((ℤRHom‘𝑌)‘(𝑧 · 𝑤)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑧 · 𝑤))) |
53 | 48, 52 | bitr3d 190 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
((((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑧 · 𝑤))) |
54 | 4, 28, 50 | zndvds0 14095 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑧)) |
55 | 3, 41, 54 | syl2an2r 595 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
(((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑧)) |
56 | 4, 28, 50 | zndvds0 14095 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑤 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑤)) |
57 | 3, 42, 56 | syl2an2r 595 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
(((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑤)) |
58 | 55, 57 | orbi12d 794 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
((((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌)) ↔ (𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤))) |
59 | 37, 53, 58 | 3bitr4d 220 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
((((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌)))) |
60 | 59 | biimpd 144 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) →
((((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌) → (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌)))) |
61 | | oveq12 5915 |
. . . . . . . . . . 11
⊢ ((𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → (𝑥(.r‘𝑌)𝑦) = (((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤))) |
62 | 61 | eqeq1d 2198 |
. . . . . . . . . 10
⊢ ((𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌))) |
63 | | eqeq1 2196 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (0g‘𝑌) ↔ ((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌))) |
64 | 63 | orbi1d 792 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → ((𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)) ↔ (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)))) |
65 | | eqeq1 2196 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((ℤRHom‘𝑌)‘𝑤) → (𝑦 = (0g‘𝑌) ↔ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌))) |
66 | 65 | orbi2d 791 |
. . . . . . . . . . 11
⊢ (𝑦 = ((ℤRHom‘𝑌)‘𝑤) → ((((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)) ↔ (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌)))) |
67 | 64, 66 | sylan9bb 462 |
. . . . . . . . . 10
⊢ ((𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → ((𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)) ↔ (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌)))) |
68 | 62, 67 | imbi12d 234 |
. . . . . . . . 9
⊢ ((𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → (((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌))) ↔ ((((ℤRHom‘𝑌)‘𝑧)(.r‘𝑌)((ℤRHom‘𝑌)‘𝑤)) = (0g‘𝑌) → (((ℤRHom‘𝑌)‘𝑧) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑤) = (0g‘𝑌))))) |
69 | 60, 68 | syl5ibrcom 157 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ)) → ((𝑥 = ((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌))))) |
70 | 69 | rexlimdvva 2615 |
. . . . . . 7
⊢ (𝑁 ∈ ℙ →
(∃𝑧 ∈ ℤ
∃𝑤 ∈ ℤ
(𝑥 =
((ℤRHom‘𝑌)‘𝑧) ∧ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌))))) |
71 | 35, 70 | biimtrrid 153 |
. . . . . 6
⊢ (𝑁 ∈ ℙ →
((∃𝑧 ∈ ℤ
𝑥 =
((ℤRHom‘𝑌)‘𝑧) ∧ ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤)) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌))))) |
72 | 71 | imp 124 |
. . . . 5
⊢ ((𝑁 ∈ ℙ ∧
(∃𝑧 ∈ ℤ
𝑥 =
((ℤRHom‘𝑌)‘𝑧) ∧ ∃𝑤 ∈ ℤ 𝑦 = ((ℤRHom‘𝑌)‘𝑤))) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)))) |
73 | 34, 72 | syldan 282 |
. . . 4
⊢ ((𝑁 ∈ ℙ ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)))) |
74 | 73 | ralrimivva 2572 |
. . 3
⊢ (𝑁 ∈ ℙ →
∀𝑥 ∈
(Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌)))) |
75 | 13, 45, 50 | isdomn 13729 |
. . 3
⊢ (𝑌 ∈ Domn ↔ (𝑌 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)𝑦) = (0g‘𝑌) → (𝑥 = (0g‘𝑌) ∨ 𝑦 = (0g‘𝑌))))) |
76 | 27, 74, 75 | sylanbrc 417 |
. 2
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Domn) |
77 | | isidom 13736 |
. 2
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
78 | 6, 76, 77 | sylanbrc 417 |
1
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ IDomn) |