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 ) |`s ( Unit ` R ) )
proot1mul.o 
|- O = ( od ` G )
proot1mul.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion proot1mul 
|- ( ( ( R e. IDomn /\ N e. NN ) /\ ( X e. ( `' O " { N } ) /\ Y e. ( `' O " { N } ) ) ) -> X e. ( K ` { Y } ) )

Proof

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