idomodle

Description: Limit on the number of N -th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	idomodle.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
	idomodle.b	$⊢ B = {Base}_{G}$
	idomodle.o	$⊢ O = od (G)$
Assertion	idomodle	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| O (x) ∥ N\}\| \leq N$

Proof

Step	Hyp	Ref	Expression
1		idomodle.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
2		idomodle.b	$⊢ B = {Base}_{G}$
3		idomodle.o	$⊢ O = od (G)$
4	2	fvexi	$⊢ B \in V$
5	4	rabex	$⊢ \{x \in B \| O (x) ∥ N\} \in V$
6		hashxrcl	$⊢ \{x \in B \| O (x) ∥ N\} \in V \to \|\{x \in B \| O (x) ∥ N\}\| \in ℝ^{*}$
7	5 6	mp1i	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| O (x) ∥ N\}\| \in ℝ^{*}$
8		fvex	$⊢ {Base}_{R} \in V$
9	8	rabex	$⊢ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \in V$
10		hashxrcl	$⊢ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \in V \to \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \in ℝ^{*}$
11	9 10	mp1i	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \in ℝ^{*}$
12		nnre	$⊢ N \in ℕ \to N \in ℝ$
13	12	rexrd	$⊢ N \in ℕ \to N \in ℝ^{*}$
14	13	adantl	$⊢ (R \in IDomn \land N \in ℕ) \to N \in ℝ^{*}$
15		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
16	15	simplbi	$⊢ R \in IDomn \to R \in CRing$
17	16	adantr	$⊢ (R \in IDomn \land N \in ℕ) \to R \in CRing$
18		crngring	$⊢ R \in CRing \to R \in Ring$
19	17 18	syl	$⊢ (R \in IDomn \land N \in ℕ) \to R \in Ring$
20	19	adantr	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to R \in Ring$
21		eqid	$⊢ Unit (R) = Unit (R)$
22	21 1	unitgrp	$⊢ R \in Ring \to G \in Grp$
23	20 22	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to G \in Grp$
24		simpr	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to x \in B$
25		nnz	$⊢ N \in ℕ \to N \in ℤ$
26	25	ad2antlr	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to N \in ℤ$
27		eqid	$⊢ \cdot_{G} = \cdot_{G}$
28		eqid	$⊢ 0_{G} = 0_{G}$
29	2 3 27 28	oddvds	$⊢ (G \in Grp \land x \in B \land N \in ℤ) \to (O (x) ∥ N \leftrightarrow N \cdot_{G} x = 0_{G})$
30	23 24 26 29	syl3anc	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to (O (x) ∥ N \leftrightarrow N \cdot_{G} x = 0_{G})$
31		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
32	21 31	unitsubm	$⊢ R \in Ring \to Unit (R) \in SubMnd ({mulGrp}_{R})$
33	20 32	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to Unit (R) \in SubMnd ({mulGrp}_{R})$
34		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
35	34	ad2antlr	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to N \in ℕ_{0}$
36	21 1	unitgrpbas	$⊢ Unit (R) = {Base}_{G}$
37	2 36	eqtr4i	$⊢ B = Unit (R)$
38	24 37	eleqtrdi	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to x \in Unit (R)$
39		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
40	39 1 27	submmulg	$⊢ (Unit (R) \in SubMnd ({mulGrp}_{R}) \land N \in ℕ_{0} \land x \in Unit (R)) \to N \cdot_{{mulGrp}_{R}} x = N \cdot_{G} x$
41	33 35 38 40	syl3anc	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to N \cdot_{{mulGrp}_{R}} x = N \cdot_{G} x$
42		eqid	$⊢ 1_{R} = 1_{R}$
43	21 1 42	unitgrpid	$⊢ R \in Ring \to 1_{R} = 0_{G}$
44	20 43	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to 1_{R} = 0_{G}$
45	41 44	eqeq12d	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to (N \cdot_{{mulGrp}_{R}} x = 1_{R} \leftrightarrow N \cdot_{G} x = 0_{G})$
46	30 45	bitr4d	$⊢ ((R \in IDomn \land N \in ℕ) \land x \in B) \to (O (x) ∥ N \leftrightarrow N \cdot_{{mulGrp}_{R}} x = 1_{R})$
47	46	rabbidva	$⊢ (R \in IDomn \land N \in ℕ) \to \{x \in B \| O (x) ∥ N\} = \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}$
48	47	fveq2d	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| O (x) ∥ N\}\| = \|\{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\|$
49		eqid	$⊢ {Base}_{R} = {Base}_{R}$
50	49 37	unitss	$⊢ B \subseteq {Base}_{R}$
51		rabss2	$⊢ B \subseteq {Base}_{R} \to \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \subseteq \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}$
52	50 51	mp1i	$⊢ (R \in IDomn \land N \in ℕ) \to \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \subseteq \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}$
53		ssdomg	$⊢ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \in V \to (\{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \subseteq \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \to \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} ≼ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\})$
54	9 52 53	mpsyl	$⊢ (R \in IDomn \land N \in ℕ) \to \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} ≼ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}$
55		hashdomi	$⊢ \{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} ≼ \{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\} \to \|\{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \leq \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\|$
56	54 55	syl	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \leq \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\|$
57	48 56	eqbrtrd	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| O (x) ∥ N\}\| \leq \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\|$
58		simpl	$⊢ (R \in IDomn \land N \in ℕ) \to R \in IDomn$
59	49 42	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
60	19 59	syl	$⊢ (R \in IDomn \land N \in ℕ) \to 1_{R} \in {Base}_{R}$
61		simpr	$⊢ (R \in IDomn \land N \in ℕ) \to N \in ℕ$
62	49 39	idomrootle	$⊢ (R \in IDomn \land 1_{R} \in {Base}_{R} \land N \in ℕ) \to \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \leq N$
63	58 60 61 62	syl3anc	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in {Base}_{R} \| N \cdot_{{mulGrp}_{R}} x = 1_{R}\}\| \leq N$
64	7 11 14 57 63	xrletrd	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{x \in B \| O (x) ∥ N\}\| \leq N$

Metamath Proof Explorer

Theorem idomodle

Proof