This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znfld

Description: The Z/nZ structure is a finite field when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion znfld ( 𝑁 ∈ ℙ → 𝑌 ∈ Field )

Proof

Step Hyp Ref Expression
1 zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 prmnn ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
3 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4 2 3 syl ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ0 )
5 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
6 4 5 syl ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ CRing )
7 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
8 2 3 5 7 4syl ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ Ring )
9 hash2 ⊢ ( ♯ ‘ 2o ) = 2
10 prmuz2 ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
11 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
12 10 11 syl ⊢ ( 𝑁 ∈ ℙ → 2 ≤ 𝑁 )
13 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
14 1 13 znhash ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( Base ‘ 𝑌 ) ) = 𝑁 )
15 2 14 syl ⊢ ( 𝑁 ∈ ℙ → ( ♯ ‘ ( Base ‘ 𝑌 ) ) = 𝑁 )
16 12 15 breqtrrd ⊢ ( 𝑁 ∈ ℙ → 2 ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) )
17 9 16 eqbrtrid ⊢ ( 𝑁 ∈ ℙ → ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) )
18 2onn ⊢ 2o ∈ ω
19 nnfi ⊢ ( 2o ∈ ω → 2o ∈ Fin )
20 18 19 ax-mp ⊢ 2o ∈ Fin
21 fvex ⊢ ( Base ‘ 𝑌 ) ∈ V
22 hashdom ⊢ ( ( 2o ∈ Fin ∧ ( Base ‘ 𝑌 ) ∈ V ) → ( ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) ↔ 2o ≼ ( Base ‘ 𝑌 ) ) )
23 20 21 22 mp2an ⊢ ( ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) ↔ 2o ≼ ( Base ‘ 𝑌 ) )
24 17 23 sylib ⊢ ( 𝑁 ∈ ℙ → 2o ≼ ( Base ‘ 𝑌 ) )
25 13 isnzr2 ⊢ ( 𝑌 ∈ NzRing ↔ ( 𝑌 ∈ Ring ∧ 2o ≼ ( Base ‘ 𝑌 ) ) )
26 8 24 25 sylanbrc ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ NzRing )
27 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
28 1 13 27 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) )
29 4 28 syl ⊢ ( 𝑁 ∈ ℙ → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) )
30 foelrn ⊢ ( ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ 𝑥 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) )
31 foelrn ⊢ ( ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) )
32 30 31 anim12dan ⊢ ( ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ) ) → ( ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
33 29 32 sylan ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ) ) → ( ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
34 reeanv ⊢ ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) ↔ ( ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
35 euclemma ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( 𝑁 ∥ ( 𝑧 · 𝑤 ) ↔ ( 𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤 ) ) )
36 35 3expb ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝑧 · 𝑤 ) ↔ ( 𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤 ) ) )
37 8 adantr ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → 𝑌 ∈ Ring )
38 27 zrhrhm ⊢ ( 𝑌 ∈ Ring → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
39 37 38 syl ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
40 simprl ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → 𝑧 ∈ ℤ )
41 simprr ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → 𝑤 ∈ ℤ )
42 zringbas ⊢ ℤ = ( Base ‘ ℤring )
43 zringmulr ⊢ · = ( .r ‘ ℤring )
44 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
45 42 43 44 rhmmul ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) ∧ 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 · 𝑤 ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
46 39 40 41 45 syl3anc ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 · 𝑤 ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
47 46 eqeq1d ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 · 𝑤 ) ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) ) )
48 zmulcl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( 𝑧 · 𝑤 ) ∈ ℤ )
49 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
50 1 27 49 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑧 · 𝑤 ) ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 · 𝑤 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑧 · 𝑤 ) ) )
51 4 48 50 syl2an ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 · 𝑤 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑧 · 𝑤 ) ) )
52 47 51 bitr3d ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑧 · 𝑤 ) ) )
53 1 27 49 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑧 ) )
54 4 40 53 syl2an2r ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑧 ) )
55 1 27 49 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑤 ) )
56 4 41 55 syl2an2r ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑤 ) )
57 54 56 orbi12d ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ↔ ( 𝑁 ∥ 𝑧 ∨ 𝑁 ∥ 𝑤 ) ) )
58 36 52 57 3bitr4d ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ) )
59 58 biimpd ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ) )
60 oveq12 ⊢ ( ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) )
61 60 eqeq1d ⊢ ( ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) ) )
62 eqeq1 ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ) )
63 62 orbi1d ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) → ( ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) )
64 eqeq1 ⊢ ( 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) → ( 𝑦 = ( 0g ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) )
65 64 orbi2d ⊢ ( 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ) )
66 63 65 sylan9bb ⊢ ( ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ) )
67 61 66 imbi12d ⊢ ( ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) ↔ ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑌 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) = ( 0g ‘ 𝑌 ) ) ) ) )
68 59 67 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) ) )
69 68 rexlimdvva ⊢ ( 𝑁 ∈ ℙ → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) ) )
70 34 69 biimtrrid ⊢ ( 𝑁 ∈ ℙ → ( ( ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) ) )
71 70 imp ⊢ ( ( 𝑁 ∈ ℙ ∧ ( ∃ 𝑧 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ∧ ∃ 𝑤 ∈ ℤ 𝑦 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑤 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) )
72 33 71 syldan ⊢ ( ( 𝑁 ∈ ℙ ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) )
73 72 ralrimivva ⊢ ( 𝑁 ∈ ℙ → ∀ 𝑥 ∈ ( Base ‘ 𝑌 ) ∀ 𝑦 ∈ ( Base ‘ 𝑌 ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) )
74 13 44 49 isdomn ⊢ ( 𝑌 ∈ Domn ↔ ( 𝑌 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑌 ) ∀ 𝑦 ∈ ( Base ‘ 𝑌 ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) = ( 0g ‘ 𝑌 ) → ( 𝑥 = ( 0g ‘ 𝑌 ) ∨ 𝑦 = ( 0g ‘ 𝑌 ) ) ) ) )
75 26 73 74 sylanbrc ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ Domn )
76 isidom ⊢ ( 𝑌 ∈ IDomn ↔ ( 𝑌 ∈ CRing ∧ 𝑌 ∈ Domn ) )
77 6 75 76 sylanbrc ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ IDomn )
78 1 13 znfi ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ 𝑌 ) ∈ Fin )
79 2 78 syl ⊢ ( 𝑁 ∈ ℙ → ( Base ‘ 𝑌 ) ∈ Fin )
80 13 fiidomfld ⊢ ( ( Base ‘ 𝑌 ) ∈ Fin → ( 𝑌 ∈ IDomn ↔ 𝑌 ∈ Field ) )
81 79 80 syl ⊢ ( 𝑁 ∈ ℙ → ( 𝑌 ∈ IDomn ↔ 𝑌 ∈ Field ) )
82 77 81 mpbid ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ Field )