Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  idomodle Structured version   Visualization version   GIF version

Theorem idomodle 38275
Description: Limit on the number of 𝑁-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.)
Hypotheses
Ref Expression
idomodle.g 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))
idomodle.b 𝐵 = (Base‘𝐺)
idomodle.o 𝑂 = (od‘𝐺)
Assertion
Ref Expression
idomodle ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) ≤ 𝑁)
Distinct variable groups:   𝑥,𝐵   𝑥,𝑁   𝑥,𝑅
Allowed substitution hints:   𝐺(𝑥)   𝑂(𝑥)

Proof of Theorem idomodle
StepHypRef Expression
1 idomodle.b . . . . 5 𝐵 = (Base‘𝐺)
21fvexi 6422 . . . 4 𝐵 ∈ V
32rabex 5007 . . 3 {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁} ∈ V
4 hashxrcl 13366 . . 3 ({𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁} ∈ V → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) ∈ ℝ*)
53, 4mp1i 13 . 2 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) ∈ ℝ*)
6 fvex 6421 . . . 4 (Base‘𝑅) ∈ V
76rabex 5007 . . 3 {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ∈ V
8 hashxrcl 13366 . . 3 ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ∈ V → (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ∈ ℝ*)
97, 8mp1i 13 . 2 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ∈ ℝ*)
10 nnre 11312 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1110rexrd 10374 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ*)
1211adantl 469 . 2 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ*)
13 isidom 19513 . . . . . . . . . . . 12 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
1413simplbi 487 . . . . . . . . . . 11 (𝑅 ∈ IDomn → 𝑅 ∈ CRing)
1514adantr 468 . . . . . . . . . 10 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ CRing)
16 crngring 18760 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
1715, 16syl 17 . . . . . . . . 9 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Ring)
1817adantr 468 . . . . . . . 8 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝑅 ∈ Ring)
19 eqid 2806 . . . . . . . . 9 (Unit‘𝑅) = (Unit‘𝑅)
20 idomodle.g . . . . . . . . 9 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))
2119, 20unitgrp 18869 . . . . . . . 8 (𝑅 ∈ Ring → 𝐺 ∈ Grp)
2218, 21syl 17 . . . . . . 7 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝐺 ∈ Grp)
23 simpr 473 . . . . . . 7 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝑥𝐵)
24 nnz 11665 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
2524ad2antlr 709 . . . . . . 7 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝑁 ∈ ℤ)
26 idomodle.o . . . . . . . 8 𝑂 = (od‘𝐺)
27 eqid 2806 . . . . . . . 8 (.g𝐺) = (.g𝐺)
28 eqid 2806 . . . . . . . 8 (0g𝐺) = (0g𝐺)
291, 26, 27, 28oddvds 18167 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑥𝐵𝑁 ∈ ℤ) → ((𝑂𝑥) ∥ 𝑁 ↔ (𝑁(.g𝐺)𝑥) = (0g𝐺)))
3022, 23, 25, 29syl3anc 1483 . . . . . 6 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → ((𝑂𝑥) ∥ 𝑁 ↔ (𝑁(.g𝐺)𝑥) = (0g𝐺)))
31 eqid 2806 . . . . . . . . . 10 (mulGrp‘𝑅) = (mulGrp‘𝑅)
3219, 31unitsubm 18872 . . . . . . . . 9 (𝑅 ∈ Ring → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅)))
3318, 32syl 17 . . . . . . . 8 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅)))
34 nnnn0 11566 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
3534ad2antlr 709 . . . . . . . 8 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝑁 ∈ ℕ0)
3619, 20unitgrpbas 18868 . . . . . . . . . 10 (Unit‘𝑅) = (Base‘𝐺)
371, 36eqtr4i 2831 . . . . . . . . 9 𝐵 = (Unit‘𝑅)
3823, 37syl6eleq 2895 . . . . . . . 8 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → 𝑥 ∈ (Unit‘𝑅))
39 eqid 2806 . . . . . . . . 9 (.g‘(mulGrp‘𝑅)) = (.g‘(mulGrp‘𝑅))
4039, 20, 27submmulg 17788 . . . . . . . 8 (((Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑁 ∈ ℕ0𝑥 ∈ (Unit‘𝑅)) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g𝐺)𝑥))
4133, 35, 38, 40syl3anc 1483 . . . . . . 7 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g𝐺)𝑥))
42 eqid 2806 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
4319, 20, 42unitgrpid 18871 . . . . . . . 8 (𝑅 ∈ Ring → (1r𝑅) = (0g𝐺))
4418, 43syl 17 . . . . . . 7 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → (1r𝑅) = (0g𝐺))
4541, 44eqeq12d 2821 . . . . . 6 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → ((𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅) ↔ (𝑁(.g𝐺)𝑥) = (0g𝐺)))
4630, 45bitr4d 273 . . . . 5 (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥𝐵) → ((𝑂𝑥) ∥ 𝑁 ↔ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)))
4746rabbidva 3378 . . . 4 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁} = {𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)})
4847fveq2d 6412 . . 3 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) = (♯‘{𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}))
49 eqid 2806 . . . . . . 7 (Base‘𝑅) = (Base‘𝑅)
5049, 37unitss 18862 . . . . . 6 𝐵 ⊆ (Base‘𝑅)
51 rabss2 3882 . . . . . 6 (𝐵 ⊆ (Base‘𝑅) → {𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)})
5250, 51mp1i 13 . . . . 5 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)})
53 ssdomg 8238 . . . . 5 ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ∈ V → ({𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} → {𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}))
547, 52, 53mpsyl 68 . . . 4 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)})
55 hashdomi 13387 . . . 4 ({𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)} → (♯‘{𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}))
5654, 55syl 17 . . 3 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}))
5748, 56eqbrtrd 4866 . 2 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}))
58 simpl 470 . . 3 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ IDomn)
5949, 42ringidcl 18770 . . . 4 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
6017, 59syl 17 . . 3 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (1r𝑅) ∈ (Base‘𝑅))
61 simpr 473 . . 3 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
6249, 39idomrootle 38274 . . 3 ((𝑅 ∈ IDomn ∧ (1r𝑅) ∈ (Base‘𝑅) ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ≤ 𝑁)
6358, 60, 61, 62syl3anc 1483 . 2 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r𝑅)}) ≤ 𝑁)
645, 9, 12, 57, 63xrletrd 12211 1 ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}) ≤ 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  {crab 3100  Vcvv 3391  wss 3769   class class class wbr 4844  cfv 6101  (class class class)co 6874  cdom 8190  *cxr 10358  cle 10360  cn 11305  0cn0 11559  cz 11643  chash 13337  cdvds 15203  Basecbs 16068  s cress 16069  0gc0g 16305  SubMndcsubmnd 17539  Grpcgrp 17627  .gcmg 17745  odcod 18145  mulGrpcmgp 18691  1rcur 18703  Ringcrg 18749  CRingccrg 18750  Unitcui 18841  Domncdomn 19489  IDomncidom 19490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-ofr 7128  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-tpos 7587  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-xnn0 11630  df-z 11644  df-dec 11760  df-uz 11905  df-rp 12047  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-hash 13338  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-dvds 15204  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-0g 16307  df-gsum 16308  df-prds 16313  df-pws 16315  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-mhm 17540  df-submnd 17541  df-grp 17630  df-minusg 17631  df-sbg 17632  df-mulg 17746  df-subg 17793  df-ghm 17860  df-cntz 17951  df-od 18149  df-cmn 18396  df-abl 18397  df-mgp 18692  df-ur 18704  df-srg 18708  df-ring 18751  df-cring 18752  df-oppr 18825  df-dvdsr 18843  df-unit 18844  df-invr 18874  df-rnghom 18919  df-subrg 18982  df-lmod 19069  df-lss 19137  df-lsp 19179  df-nzr 19467  df-rlreg 19492  df-domn 19493  df-idom 19494  df-assa 19521  df-asp 19522  df-ascl 19523  df-psr 19565  df-mvr 19566  df-mpl 19567  df-opsr 19569  df-evls 19714  df-evl 19715  df-psr1 19758  df-vr1 19759  df-ply1 19760  df-coe1 19761  df-evl1 19889  df-cnfld 19955  df-mdeg 24029  df-deg1 24030  df-mon1 24104  df-uc1p 24105  df-q1p 24106  df-r1p 24107
This theorem is referenced by:  idomsubgmo  38277
  Copyright terms: Public domain W3C validator