Theorem 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	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
	idomodle.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	idomodle.o	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	idomodle	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		idomodle.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
2		idomodle.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		idomodle.o	⊢ 𝑂 = ( od ‘ 𝐺 )
4	2	fvexi	⊢ 𝐵 ∈ V
5	4	rabex	⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ V
6		hashxrcl	⊢ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ V → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ∈ ℝ* )
7	5 6	mp1i	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ∈ ℝ* )
8		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
9	8	rabex	⊢ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ∈ V
10		hashxrcl	⊢ ( { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ∈ V → ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ∈ ℝ* )
11	9 10	mp1i	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ∈ ℝ* )
12		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
13	12	rexrd	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ* )
14	13	adantl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ* )
15		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
16	15	simplbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
17	16	adantr	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → 𝑅 ∈ CRing )
18		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
19	17 18	syl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → 𝑅 ∈ Ring )
20	19	adantr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
21		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
22	21 1	unitgrp	⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
23	20 22	syl	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝐺 ∈ Grp )
24		simpr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
25		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
26	25	ad2antlr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
27		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
28		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
29	2 3 27 28	oddvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
30	23 24 26 29	syl3anc	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
31		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
32	21 31	unitsubm	⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
33	20 32	syl	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
34		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
35	34	ad2antlr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ℕ0 )
36	21 1	unitgrpbas	⊢ ( Unit ‘ 𝑅 ) = ( Base ‘ 𝐺 )
37	2 36	eqtr4i	⊢ 𝐵 = ( Unit ‘ 𝑅 )
38	24 37	eleqtrdi	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
39		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
40	39 1 27	submmulg	⊢ ( ( ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) )
41	33 35 38 40	syl3anc	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) )
42		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
43	21 1 42	unitgrpid	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) )
44	20 43	syl	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) )
45	41 44	eqeq12d	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
46	30 45	bitr4d	⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
47	46	rabbidva	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } = { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } )
48	47	fveq2d	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) )
49		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
50	49 37	unitss	⊢ 𝐵 ⊆ ( Base ‘ 𝑅 )
51		rabss2	⊢ ( 𝐵 ⊆ ( Base ‘ 𝑅 ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ⊆ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } )
52	50 51	mp1i	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ⊆ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } )
53		ssdomg	⊢ ( { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ∈ V → ( { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ⊆ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } → { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ≼ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) )
54	9 52 53	mpsyl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ≼ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } )
55		hashdomi	⊢ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ≼ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ≤ ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) )
56	54 55	syl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ≤ ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) )
57	48 56	eqbrtrd	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ≤ ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) )
58		simpl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → 𝑅 ∈ IDomn )
59	49 42	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
60	19 59	syl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
61		simpr	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
62	49 39	idomrootle	⊢ ( ( 𝑅 ∈ IDomn ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ≤ 𝑁 )
63	58 60 61 62	syl3anc	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) } ) ≤ 𝑁 )
64	7 11 14 57 63	xrletrd	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ≤ 𝑁 )