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 )