dchrfi

Description: The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	dchrabl.g	$⊢ G = DChr (N)$
	dchrfi.b	$⊢ D = {Base}_{G}$
Assertion	dchrfi	$⊢ N \in ℕ \to D \in Fin$

Proof

Step	Hyp	Ref	Expression
1		dchrabl.g	$⊢ G = DChr (N)$
2		dchrfi.b	$⊢ D = {Base}_{G}$
3		snfi	$⊢ \{0\} \in Fin$
4		cnex	$⊢ ℂ \in V$
5	4	a1i	$⊢ N \in ℕ \to ℂ \in V$
6		ovexd	$⊢ (N \in ℕ \land z \in ℂ) \to z^{ϕ (N)} \in V$
7		1cnd	$⊢ (N \in ℕ \land z \in ℂ) \to 1 \in ℂ$
8		eqidd	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)}) = (z \in ℂ ⟼ z^{ϕ (N)})$
9		fconstmpt	$⊢ ℂ \times \{1\} = (z \in ℂ ⟼ 1)$
10	9	a1i	$⊢ N \in ℕ \to ℂ \times \{1\} = (z \in ℂ ⟼ 1)$
11	5 6 7 8 10	offval2	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)}) -_{f} (ℂ \times \{1\}) = (z \in ℂ ⟼ z^{ϕ (N)} - 1)$
12		ssid	$⊢ ℂ \subseteq ℂ$
13	12	a1i	$⊢ N \in ℕ \to ℂ \subseteq ℂ$
14		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
15		phicl	$⊢ N \in ℕ \to ϕ (N) \in ℕ$
16	15	nnnn0d	$⊢ N \in ℕ \to ϕ (N) \in ℕ_{0}$
17		plypow	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ \land ϕ (N) \in ℕ_{0}) \to (z \in ℂ ⟼ z^{ϕ (N)}) \in Poly (ℂ)$
18	13 14 16 17	syl3anc	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)}) \in Poly (ℂ)$
19		ax-1cn	$⊢ 1 \in ℂ$
20		plyconst	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to ℂ \times \{1\} \in Poly (ℂ)$
21	12 19 20	mp2an	$⊢ ℂ \times \{1\} \in Poly (ℂ)$
22		plysubcl	$⊢ ((z \in ℂ ⟼ z^{ϕ (N)}) \in Poly (ℂ) \land ℂ \times \{1\} \in Poly (ℂ)) \to (z \in ℂ ⟼ z^{ϕ (N)}) -_{f} (ℂ \times \{1\}) \in Poly (ℂ)$
23	18 21 22	sylancl	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)}) -_{f} (ℂ \times \{1\}) \in Poly (ℂ)$
24	11 23	eqeltrrd	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) \in Poly (ℂ)$
25		0cn	$⊢ 0 \in ℂ$
26		neg1ne0	$⊢ - 1 \neq 0$
27	15	0expd	$⊢ N \in ℕ \to 0^{ϕ (N)} = 0$
28	27	oveq1d	$⊢ N \in ℕ \to 0^{ϕ (N)} - 1 = 0 - 1$
29		oveq1	$⊢ z = 0 \to z^{ϕ (N)} = 0^{ϕ (N)}$
30	29	oveq1d	$⊢ z = 0 \to z^{ϕ (N)} - 1 = 0^{ϕ (N)} - 1$
31		eqid	$⊢ (z \in ℂ ⟼ z^{ϕ (N)} - 1) = (z \in ℂ ⟼ z^{ϕ (N)} - 1)$
32		ovex	$⊢ 0^{ϕ (N)} - 1 \in V$
33	30 31 32	fvmpt	$⊢ 0 \in ℂ \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) = 0^{ϕ (N)} - 1$
34	25 33	ax-mp	$⊢ (z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) = 0^{ϕ (N)} - 1$
35		df-neg	$⊢ - 1 = 0 - 1$
36	28 34 35	3eqtr4g	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) = - 1$
37	36	neeq1d	$⊢ N \in ℕ \to ((z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) \neq 0 \leftrightarrow - 1 \neq 0)$
38	26 37	mpbiri	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) \neq 0$
39		ne0p	$⊢ (0 \in ℂ \land (z \in ℂ ⟼ z^{ϕ (N)} - 1) (0) \neq 0) \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) \neq 0_{𝑝}$
40	25 38 39	sylancr	$⊢ N \in ℕ \to (z \in ℂ ⟼ z^{ϕ (N)} - 1) \neq 0_{𝑝}$
41	31	mptiniseg	$⊢ 0 \in ℂ \to {(z \in ℂ ⟼ z^{ϕ (N)} - 1)}^{-1} [\{0\}] = \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}$
42	25 41	ax-mp	$⊢ {(z \in ℂ ⟼ z^{ϕ (N)} - 1)}^{-1} [\{0\}] = \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}$
43	42	eqcomi	$⊢ \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} = {(z \in ℂ ⟼ z^{ϕ (N)} - 1)}^{-1} [\{0\}]$
44	43	fta1	$⊢ ((z \in ℂ ⟼ z^{ϕ (N)} - 1) \in Poly (ℂ) \land (z \in ℂ ⟼ z^{ϕ (N)} - 1) \neq 0_{𝑝}) \to (\{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin \land \|\{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}\| \leq \deg ((z \in ℂ ⟼ z^{ϕ (N)} - 1)))$
45	24 40 44	syl2anc	$⊢ N \in ℕ \to (\{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin \land \|\{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}\| \leq \deg ((z \in ℂ ⟼ z^{ϕ (N)} - 1)))$
46	45	simpld	$⊢ N \in ℕ \to \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin$
47		unfi	$⊢ (\{0\} \in Fin \land \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin) \to \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin$
48	3 46 47	sylancr	$⊢ N \in ℕ \to \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin$
49		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
50		eqid	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{ℤ / N ℤ}$
51	49 50	znfi	$⊢ N \in ℕ \to {Base}_{ℤ / N ℤ} \in Fin$
52		mapfi	$⊢ (\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \in Fin \land {Base}_{ℤ / N ℤ} \in Fin) \to {(\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})}^{{Base}_{ℤ / N ℤ}} \in Fin$
53	48 51 52	syl2anc	$⊢ N \in ℕ \to {(\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})}^{{Base}_{ℤ / N ℤ}} \in Fin$
54		simpr	$⊢ (N \in ℕ \land f \in D) \to f \in D$
55	1 49 2 50 54	dchrf	$⊢ (N \in ℕ \land f \in D) \to f : {Base}_{ℤ / N ℤ} ⟶ ℂ$
56	55	ffnd	$⊢ (N \in ℕ \land f \in D) \to f Fn {Base}_{ℤ / N ℤ}$
57		df-ne	$⊢ f (x) \neq 0 \leftrightarrow \neg f (x) = 0$
58		fvex	$⊢ f (x) \in V$
59	58	elsn	$⊢ f (x) \in \{0\} \leftrightarrow f (x) = 0$
60	57 59	xchbinxr	$⊢ f (x) \neq 0 \leftrightarrow \neg f (x) \in \{0\}$
61		oveq1	$⊢ z = f (x) \to z^{ϕ (N)} = {f (x)}^{ϕ (N)}$
62	61	oveq1d	$⊢ z = f (x) \to z^{ϕ (N)} - 1 = {f (x)}^{ϕ (N)} - 1$
63	62	eqeq1d	$⊢ z = f (x) \to (z^{ϕ (N)} - 1 = 0 \leftrightarrow {f (x)}^{ϕ (N)} - 1 = 0)$
64		simpl	$⊢ (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0) \to x \in {Base}_{ℤ / N ℤ}$
65		ffvelrn	$⊢ (f : {Base}_{ℤ / N ℤ} ⟶ ℂ \land x \in {Base}_{ℤ / N ℤ}) \to f (x) \in ℂ$
66	55 64 65	syl2an	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (x) \in ℂ$
67	1 49 2	dchrmhm	$⊢ D \subseteq {mulGrp}_{ℤ / N ℤ} MndHom {mulGrp}_{ℂ_{fld}}$
68		simplr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f \in D$
69	67 68	sseldi	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f \in ({mulGrp}_{ℤ / N ℤ} MndHom {mulGrp}_{ℂ_{fld}})$
70	16	ad2antrr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \in ℕ_{0}$
71		simprl	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to x \in {Base}_{ℤ / N ℤ}$
72		eqid	$⊢ {mulGrp}_{ℤ / N ℤ} = {mulGrp}_{ℤ / N ℤ}$
73	72 50	mgpbas	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{{mulGrp}_{ℤ / N ℤ}}$
74		eqid	$⊢ \cdot_{{mulGrp}_{ℤ / N ℤ}} = \cdot_{{mulGrp}_{ℤ / N ℤ}}$
75		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
76	73 74 75	mhmmulg	$⊢ (f \in ({mulGrp}_{ℤ / N ℤ} MndHom {mulGrp}_{ℂ_{fld}}) \land ϕ (N) \in ℕ_{0} \land x \in {Base}_{ℤ / N ℤ}) \to f (ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x) = ϕ (N) \cdot_{{mulGrp}_{ℂ_{fld}}} f (x)$
77	69 70 71 76	syl3anc	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x) = ϕ (N) \cdot_{{mulGrp}_{ℂ_{fld}}} f (x)$
78		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
79	49	zncrng	$⊢ N \in ℕ_{0} \to ℤ / N ℤ \in CRing$
80	78 79	syl	$⊢ N \in ℕ \to ℤ / N ℤ \in CRing$
81		crngring	$⊢ ℤ / N ℤ \in CRing \to ℤ / N ℤ \in Ring$
82	80 81	syl	$⊢ N \in ℕ \to ℤ / N ℤ \in Ring$
83	82	ad2antrr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ℤ / N ℤ \in Ring$
84		eqid	$⊢ Unit (ℤ / N ℤ) = Unit (ℤ / N ℤ)$
85		eqid	$⊢ {mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ) = {mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)$
86	84 85	unitgrp	$⊢ ℤ / N ℤ \in Ring \to {mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ) \in Grp$
87	83 86	syl	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to {mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ) \in Grp$
88	49 84	znunithash	$⊢ N \in ℕ \to \|Unit (ℤ / N ℤ)\| = ϕ (N)$
89	88 16	eqeltrd	$⊢ N \in ℕ \to \|Unit (ℤ / N ℤ)\| \in ℕ_{0}$
90		fvex	$⊢ Unit (ℤ / N ℤ) \in V$
91		hashclb	$⊢ Unit (ℤ / N ℤ) \in V \to (Unit (ℤ / N ℤ) \in Fin \leftrightarrow \|Unit (ℤ / N ℤ)\| \in ℕ_{0})$
92	90 91	ax-mp	$⊢ Unit (ℤ / N ℤ) \in Fin \leftrightarrow \|Unit (ℤ / N ℤ)\| \in ℕ_{0}$
93	89 92	sylibr	$⊢ N \in ℕ \to Unit (ℤ / N ℤ) \in Fin$
94	93	ad2antrr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to Unit (ℤ / N ℤ) \in Fin$
95		simprr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (x) \neq 0$
96	1 49 2 50 84 68 71	dchrn0	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to (f (x) \neq 0 \leftrightarrow x \in Unit (ℤ / N ℤ))$
97	95 96	mpbid	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to x \in Unit (ℤ / N ℤ)$
98	84 85	unitgrpbas	$⊢ Unit (ℤ / N ℤ) = {Base}_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
99		eqid	$⊢ od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) = od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))$
100	98 99	oddvds2	$⊢ ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ) \in Grp \land Unit (ℤ / N ℤ) \in Fin \land x \in Unit (ℤ / N ℤ)) \to od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) (x) ∥ \|Unit (ℤ / N ℤ)\|$
101	87 94 97 100	syl3anc	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) (x) ∥ \|Unit (ℤ / N ℤ)\|$
102	88	ad2antrr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to \|Unit (ℤ / N ℤ)\| = ϕ (N)$
103	101 102	breqtrd	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) (x) ∥ ϕ (N)$
104	15	ad2antrr	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \in ℕ$
105	104	nnzd	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \in ℤ$
106		eqid	$⊢ \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} = \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
107		eqid	$⊢ 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
108	98 99 106 107	oddvds	$⊢ ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ) \in Grp \land x \in Unit (ℤ / N ℤ) \land ϕ (N) \in ℤ) \to (od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) (x) ∥ ϕ (N) \leftrightarrow ϕ (N) \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} x = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))})$
109	87 97 105 108	syl3anc	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to (od ({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ)) (x) ∥ ϕ (N) \leftrightarrow ϕ (N) \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} x = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))})$
110	103 109	mpbid	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} x = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
111	84 72	unitsubm	$⊢ ℤ / N ℤ \in Ring \to Unit (ℤ / N ℤ) \in SubMnd ({mulGrp}_{ℤ / N ℤ})$
112	83 111	syl	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to Unit (ℤ / N ℤ) \in SubMnd ({mulGrp}_{ℤ / N ℤ})$
113	74 85 106	submmulg	$⊢ (Unit (ℤ / N ℤ) \in SubMnd ({mulGrp}_{ℤ / N ℤ}) \land ϕ (N) \in ℕ_{0} \land x \in Unit (ℤ / N ℤ)) \to ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x = ϕ (N) \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} x$
114	112 70 97 113	syl3anc	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x = ϕ (N) \cdot_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))} x$
115		eqid	$⊢ 1_{ℤ / N ℤ} = 1_{ℤ / N ℤ}$
116	72 115	ringidval	$⊢ 1_{ℤ / N ℤ} = 0_{{mulGrp}_{ℤ / N ℤ}}$
117	85 116	subm0	$⊢ Unit (ℤ / N ℤ) \in SubMnd ({mulGrp}_{ℤ / N ℤ}) \to 1_{ℤ / N ℤ} = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
118	112 117	syl	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to 1_{ℤ / N ℤ} = 0_{({mulGrp}_{ℤ / N ℤ} ↾_{𝑠} Unit (ℤ / N ℤ))}$
119	110 114 118	3eqtr4d	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x = 1_{ℤ / N ℤ}$
120	119	fveq2d	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (ϕ (N) \cdot_{{mulGrp}_{ℤ / N ℤ}} x) = f (1_{ℤ / N ℤ})$
121	77 120	eqtr3d	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \cdot_{{mulGrp}_{ℂ_{fld}}} f (x) = f (1_{ℤ / N ℤ})$
122		cnfldexp	$⊢ (f (x) \in ℂ \land ϕ (N) \in ℕ_{0}) \to ϕ (N) \cdot_{{mulGrp}_{ℂ_{fld}}} f (x) = {f (x)}^{ϕ (N)}$
123	66 70 122	syl2anc	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to ϕ (N) \cdot_{{mulGrp}_{ℂ_{fld}}} f (x) = {f (x)}^{ϕ (N)}$
124		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
125		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
126	124 125	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
127	116 126	mhm0	$⊢ f \in ({mulGrp}_{ℤ / N ℤ} MndHom {mulGrp}_{ℂ_{fld}}) \to f (1_{ℤ / N ℤ}) = 1$
128	69 127	syl	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (1_{ℤ / N ℤ}) = 1$
129	121 123 128	3eqtr3d	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to {f (x)}^{ϕ (N)} = 1$
130	129	oveq1d	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to {f (x)}^{ϕ (N)} - 1 = 1 - 1$
131		1m1e0	$⊢ 1 - 1 = 0$
132	130 131	eqtrdi	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to {f (x)}^{ϕ (N)} - 1 = 0$
133	63 66 132	elrabd	$⊢ ((N \in ℕ \land f \in D) \land (x \in {Base}_{ℤ / N ℤ} \land f (x) \neq 0)) \to f (x) \in \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}$
134	133	expr	$⊢ ((N \in ℕ \land f \in D) \land x \in {Base}_{ℤ / N ℤ}) \to (f (x) \neq 0 \to f (x) \in \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
135	60 134	syl5bir	$⊢ ((N \in ℕ \land f \in D) \land x \in {Base}_{ℤ / N ℤ}) \to (\neg f (x) \in \{0\} \to f (x) \in \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
136	135	orrd	$⊢ ((N \in ℕ \land f \in D) \land x \in {Base}_{ℤ / N ℤ}) \to (f (x) \in \{0\} \lor f (x) \in \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
137		elun	$⊢ f (x) \in (\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}) \leftrightarrow (f (x) \in \{0\} \lor f (x) \in \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
138	136 137	sylibr	$⊢ ((N \in ℕ \land f \in D) \land x \in {Base}_{ℤ / N ℤ}) \to f (x) \in (\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
139	138	ralrimiva	$⊢ (N \in ℕ \land f \in D) \to \forall x \in {Base}_{ℤ / N ℤ} f (x) \in (\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
140		ffnfv	$⊢ f : {Base}_{ℤ / N ℤ} ⟶ \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\} \leftrightarrow (f Fn {Base}_{ℤ / N ℤ} \land \forall x \in {Base}_{ℤ / N ℤ} f (x) \in (\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}))$
141	56 139 140	sylanbrc	$⊢ (N \in ℕ \land f \in D) \to f : {Base}_{ℤ / N ℤ} ⟶ \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\}$
142	141	ex	$⊢ N \in ℕ \to (f \in D \to f : {Base}_{ℤ / N ℤ} ⟶ \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
143	48 51	elmapd	$⊢ N \in ℕ \to (f \in ({(\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})}^{{Base}_{ℤ / N ℤ}}) \leftrightarrow f : {Base}_{ℤ / N ℤ} ⟶ \{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})$
144	142 143	sylibrd	$⊢ N \in ℕ \to (f \in D \to f \in ({(\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})}^{{Base}_{ℤ / N ℤ}}))$
145	144	ssrdv	$⊢ N \in ℕ \to D \subseteq {(\{0\} \cup \{z \in ℂ \| z^{ϕ (N)} - 1 = 0\})}^{{Base}_{ℤ / N ℤ}}$
146	53 145	ssfid	$⊢ N \in ℕ \to D \in Fin$

Metamath Proof Explorer

Theorem dchrfi

Proof