proot1hash

Description: If an integral domain has a primitive N -th root of unity, it has exactly ( phiN ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	proot1hash.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
	proot1hash.o	$⊢ O = od (G)$
Assertion	proot1hash	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \|O^{-1} [\{N\}]\| = ϕ (N)$

Proof

Step	Hyp	Ref	Expression
1		proot1hash.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
2		proot1hash.o	$⊢ O = od (G)$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	3 2	odf	$⊢ O : {Base}_{G} ⟶ ℕ_{0}$
5		ffn	$⊢ O : {Base}_{G} ⟶ ℕ_{0} \to O Fn {Base}_{G}$
6		fniniseg2	$⊢ O Fn {Base}_{G} \to O^{-1} [\{N\}] = \{x \in {Base}_{G} \| O (x) = N\}$
7	4 5 6	mp2b	$⊢ O^{-1} [\{N\}] = \{x \in {Base}_{G} \| O (x) = N\}$
8		simp3	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to X \in O^{-1} [\{N\}]$
9		fniniseg	$⊢ O Fn {Base}_{G} \to (X \in O^{-1} [\{N\}] \leftrightarrow (X \in {Base}_{G} \land O (X) = N))$
10	4 5 9	mp2b	$⊢ X \in O^{-1} [\{N\}] \leftrightarrow (X \in {Base}_{G} \land O (X) = N)$
11	8 10	sylib	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to (X \in {Base}_{G} \land O (X) = N)$
12	11	simprd	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to O (X) = N$
13	12	eqeq2d	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to (O (x) = O (X) \leftrightarrow O (x) = N)$
14	13	rabbidv	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\} = \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = N\}$
15		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
16	15	simprbi	$⊢ R \in IDomn \to R \in Domn$
17	16	3ad2ant1	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to R \in Domn$
18		domnring	$⊢ R \in Domn \to R \in Ring$
19		eqid	$⊢ Unit (R) = Unit (R)$
20	19 1	unitgrp	$⊢ R \in Ring \to G \in Grp$
21	17 18 20	3syl	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to G \in Grp$
22	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
23		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
24	21 22 23	3syl	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to SubGrp (G) \in Moore ({Base}_{G})$
25		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
26	25	mrcssv	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to mrCls (SubGrp (G)) (\{X\}) \subseteq {Base}_{G}$
27		dfrab3ss	$⊢ mrCls (SubGrp (G)) (\{X\}) \subseteq {Base}_{G} \to \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = N\} = mrCls (SubGrp (G)) (\{X\}) \cap \{x \in {Base}_{G} \| O (x) = N\}$
28	24 26 27	3syl	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = N\} = mrCls (SubGrp (G)) (\{X\}) \cap \{x \in {Base}_{G} \| O (x) = N\}$
29		incom	$⊢ mrCls (SubGrp (G)) (\{X\}) \cap \{x \in {Base}_{G} \| O (x) = N\} = \{x \in {Base}_{G} \| O (x) = N\} \cap mrCls (SubGrp (G)) (\{X\})$
30		simpl1	$⊢ ((R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \land x \in O^{-1} [\{N\}]) \to R \in IDomn$
31		simpl2	$⊢ ((R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \land x \in O^{-1} [\{N\}]) \to N \in ℕ$
32		simpr	$⊢ ((R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \land x \in O^{-1} [\{N\}]) \to x \in O^{-1} [\{N\}]$
33		simpl3	$⊢ ((R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \land x \in O^{-1} [\{N\}]) \to X \in O^{-1} [\{N\}]$
34	1 2 25	proot1mul	$⊢ ((R \in IDomn \land N \in ℕ) \land (x \in O^{-1} [\{N\}] \land X \in O^{-1} [\{N\}])) \to x \in mrCls (SubGrp (G)) (\{X\})$
35	30 31 32 33 34	syl22anc	$⊢ ((R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \land x \in O^{-1} [\{N\}]) \to x \in mrCls (SubGrp (G)) (\{X\})$
36	35	ex	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to (x \in O^{-1} [\{N\}] \to x \in mrCls (SubGrp (G)) (\{X\}))$
37	36	ssrdv	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to O^{-1} [\{N\}] \subseteq mrCls (SubGrp (G)) (\{X\})$
38	7 37	eqsstrrid	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \{x \in {Base}_{G} \| O (x) = N\} \subseteq mrCls (SubGrp (G)) (\{X\})$
39		dfss2	$⊢ \{x \in {Base}_{G} \| O (x) = N\} \subseteq mrCls (SubGrp (G)) (\{X\}) \leftrightarrow \{x \in {Base}_{G} \| O (x) = N\} \cap mrCls (SubGrp (G)) (\{X\}) = \{x \in {Base}_{G} \| O (x) = N\}$
40	38 39	sylib	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \{x \in {Base}_{G} \| O (x) = N\} \cap mrCls (SubGrp (G)) (\{X\}) = \{x \in {Base}_{G} \| O (x) = N\}$
41	29 40	eqtrid	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to mrCls (SubGrp (G)) (\{X\}) \cap \{x \in {Base}_{G} \| O (x) = N\} = \{x \in {Base}_{G} \| O (x) = N\}$
42	14 28 41	3eqtrrd	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \{x \in {Base}_{G} \| O (x) = N\} = \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\}$
43	7 42	eqtrid	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to O^{-1} [\{N\}] = \{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\}$
44	43	fveq2d	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \|O^{-1} [\{N\}]\| = \|\{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\}\|$
45	11	simpld	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to X \in {Base}_{G}$
46		simp2	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to N \in ℕ$
47	12 46	eqeltrd	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to O (X) \in ℕ$
48	3 2 25	odngen	$⊢ (G \in Grp \land X \in {Base}_{G} \land O (X) \in ℕ) \to \|\{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\}\| = ϕ (O (X))$
49	21 45 47 48	syl3anc	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \|\{x \in mrCls (SubGrp (G)) (\{X\}) \| O (x) = O (X)\}\| = ϕ (O (X))$
50	12	fveq2d	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to ϕ (O (X)) = ϕ (N)$
51	44 49 50	3eqtrd	$⊢ (R \in IDomn \land N \in ℕ \land X \in O^{-1} [\{N\}]) \to \|O^{-1} [\{N\}]\| = ϕ (N)$

Metamath Proof Explorer

Theorem proot1hash

Proof