Metamath Proof Explorer


Theorem 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 IDomn N X O -1 N 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 O Fn Base G
6 fniniseg2 O Fn Base G O -1 N = x Base G | O x = N
7 4 5 6 mp2b O -1 N = x Base G | O x = N
8 simp3 R IDomn N X O -1 N X O -1 N
9 fniniseg O Fn Base G X O -1 N X Base G O X = N
10 4 5 9 mp2b X O -1 N X Base G O X = N
11 8 10 sylib R IDomn N X O -1 N X Base G O X = N
12 11 simprd R IDomn N X O -1 N O X = N
13 12 eqeq2d R IDomn N X O -1 N O x = O X O x = N
14 13 rabbidv R IDomn N X O -1 N x mrCls SubGrp G X | O x = O X = x mrCls SubGrp G X | O x = N
15 isidom R IDomn R CRing R Domn
16 15 simprbi R IDomn R Domn
17 16 3ad2ant1 R IDomn N X O -1 N R Domn
18 domnring R Domn R Ring
19 eqid Unit R = Unit R
20 19 1 unitgrp R Ring G Grp
21 17 18 20 3syl R IDomn N X O -1 N G Grp
22 3 subgacs G Grp SubGrp G ACS Base G
23 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
24 21 22 23 3syl R IDomn N X O -1 N SubGrp G Moore Base G
25 eqid mrCls SubGrp G = mrCls SubGrp G
26 25 mrcssv SubGrp G Moore Base G mrCls SubGrp G X Base G
27 dfrab3ss mrCls SubGrp G X Base G x mrCls SubGrp G X | O x = N = mrCls SubGrp G X x Base G | O x = N
28 24 26 27 3syl R IDomn N X O -1 N x mrCls SubGrp G X | O x = N = mrCls SubGrp G X x Base G | O x = N
29 incom mrCls SubGrp G X x Base G | O x = N = x Base G | O x = N mrCls SubGrp G X
30 simpl1 R IDomn N X O -1 N x O -1 N R IDomn
31 simpl2 R IDomn N X O -1 N x O -1 N N
32 simpr R IDomn N X O -1 N x O -1 N x O -1 N
33 simpl3 R IDomn N X O -1 N x O -1 N X O -1 N
34 1 2 25 proot1mul R IDomn N x O -1 N X O -1 N x mrCls SubGrp G X
35 30 31 32 33 34 syl22anc R IDomn N X O -1 N x O -1 N x mrCls SubGrp G X
36 35 ex R IDomn N X O -1 N x O -1 N x mrCls SubGrp G X
37 36 ssrdv R IDomn N X O -1 N O -1 N mrCls SubGrp G X
38 7 37 eqsstrrid R IDomn N X O -1 N x Base G | O x = N mrCls SubGrp G X
39 df-ss x Base G | O x = N mrCls SubGrp G X x Base G | O x = N mrCls SubGrp G X = x Base G | O x = N
40 38 39 sylib R IDomn N X O -1 N x Base G | O x = N mrCls SubGrp G X = x Base G | O x = N
41 29 40 syl5eq R IDomn N X O -1 N mrCls SubGrp G X x Base G | O x = N = x Base G | O x = N
42 14 28 41 3eqtrrd R IDomn N X O -1 N x Base G | O x = N = x mrCls SubGrp G X | O x = O X
43 7 42 syl5eq R IDomn N X O -1 N O -1 N = x mrCls SubGrp G X | O x = O X
44 43 fveq2d R IDomn N X O -1 N O -1 N = x mrCls SubGrp G X | O x = O X
45 11 simpld R IDomn N X O -1 N X Base G
46 simp2 R IDomn N X O -1 N N
47 12 46 eqeltrd R IDomn N X O -1 N O X
48 3 2 25 odngen G Grp X Base G O X x mrCls SubGrp G X | O x = O X = ϕ O X
49 21 45 47 48 syl3anc R IDomn N X O -1 N x mrCls SubGrp G X | O x = O X = ϕ O X
50 12 fveq2d R IDomn N X O -1 N ϕ O X = ϕ N
51 44 49 50 3eqtrd R IDomn N X O -1 N O -1 N = ϕ N