Metamath Proof Explorer


Theorem proot1mul

Description: Any primitive N -th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015)

Ref Expression
Hypotheses idomsubgmo.g G = mulGrp R 𝑠 Unit R
proot1mul.o O = od G
proot1mul.k K = mrCls SubGrp G
Assertion proot1mul R IDomn N X O -1 N Y O -1 N X K Y

Proof

Step Hyp Ref Expression
1 idomsubgmo.g G = mulGrp R 𝑠 Unit R
2 proot1mul.o O = od G
3 proot1mul.k K = mrCls SubGrp G
4 simpll R IDomn N X O -1 N Y O -1 N R IDomn
5 isidom R IDomn R CRing R Domn
6 5 simprbi R IDomn R Domn
7 domnring R Domn R Ring
8 eqid Unit R = Unit R
9 8 1 unitgrp R Ring G Grp
10 4 6 7 9 4syl R IDomn N X O -1 N Y O -1 N G Grp
11 eqid Base G = Base G
12 11 subgacs G Grp SubGrp G ACS Base G
13 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
14 10 12 13 3syl R IDomn N X O -1 N Y O -1 N SubGrp G Moore Base G
15 simprl R IDomn N X O -1 N Y O -1 N X O -1 N
16 11 2 odf O : Base G 0
17 ffn O : Base G 0 O Fn Base G
18 fniniseg O Fn Base G X O -1 N X Base G O X = N
19 16 17 18 mp2b X O -1 N X Base G O X = N
20 15 19 sylib R IDomn N X O -1 N Y O -1 N X Base G O X = N
21 20 simpld R IDomn N X O -1 N Y O -1 N X Base G
22 21 snssd R IDomn N X O -1 N Y O -1 N X Base G
23 14 3 22 mrcssidd R IDomn N X O -1 N Y O -1 N X K X
24 snssg X O -1 N X K X X K X
25 15 24 syl R IDomn N X O -1 N Y O -1 N X K X X K X
26 23 25 mpbird R IDomn N X O -1 N Y O -1 N X K X
27 1 idomsubgmo R IDomn N * x SubGrp G x = N
28 27 adantr R IDomn N X O -1 N Y O -1 N * x SubGrp G x = N
29 3 mrccl SubGrp G Moore Base G X Base G K X SubGrp G
30 14 22 29 syl2anc R IDomn N X O -1 N Y O -1 N K X SubGrp G
31 20 simprd R IDomn N X O -1 N Y O -1 N O X = N
32 simplr R IDomn N X O -1 N Y O -1 N N
33 31 32 eqeltrd R IDomn N X O -1 N Y O -1 N O X
34 11 2 3 odhash2 G Grp X Base G O X K X = O X
35 10 21 33 34 syl3anc R IDomn N X O -1 N Y O -1 N K X = O X
36 35 31 eqtrd R IDomn N X O -1 N Y O -1 N K X = N
37 simprr R IDomn N X O -1 N Y O -1 N Y O -1 N
38 fniniseg O Fn Base G Y O -1 N Y Base G O Y = N
39 16 17 38 mp2b Y O -1 N Y Base G O Y = N
40 37 39 sylib R IDomn N X O -1 N Y O -1 N Y Base G O Y = N
41 40 simpld R IDomn N X O -1 N Y O -1 N Y Base G
42 41 snssd R IDomn N X O -1 N Y O -1 N Y Base G
43 3 mrccl SubGrp G Moore Base G Y Base G K Y SubGrp G
44 14 42 43 syl2anc R IDomn N X O -1 N Y O -1 N K Y SubGrp G
45 40 simprd R IDomn N X O -1 N Y O -1 N O Y = N
46 45 32 eqeltrd R IDomn N X O -1 N Y O -1 N O Y
47 11 2 3 odhash2 G Grp Y Base G O Y K Y = O Y
48 10 41 46 47 syl3anc R IDomn N X O -1 N Y O -1 N K Y = O Y
49 48 45 eqtrd R IDomn N X O -1 N Y O -1 N K Y = N
50 fveqeq2 x = K X x = N K X = N
51 fveqeq2 x = K Y x = N K Y = N
52 50 51 rmoi * x SubGrp G x = N K X SubGrp G K X = N K Y SubGrp G K Y = N K X = K Y
53 28 30 36 44 49 52 syl122anc R IDomn N X O -1 N Y O -1 N K X = K Y
54 26 53 eleqtrd R IDomn N X O -1 N Y O -1 N X K Y