Metamath Proof Explorer

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 
|- G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
idomodle.b 
|- B = ( Base ` G )
idomodle.o 
|- O = ( od ` G )
Assertion idomodle 
|- ( ( R e. IDomn /\ N e. NN ) -> ( # ` { x e. B | ( O ` x ) || N } ) <_ N )

Proof

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