MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrval Structured version   Visualization version   GIF version
Theorem dchrval 26737
Description: Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
Hypotheses
Ref Expression
dchrval.g 𝐺 = (DChrβ€˜π‘)
dchrval.z 𝑍 = (β„€/nβ„€β€˜π‘)
dchrval.b 𝐡 = (Baseβ€˜π‘)
dchrval.u π‘ˆ = (Unitβ€˜π‘)
dchrval.n (πœ‘ β†’ 𝑁 ∈ β„•)
dchrval.d (πœ‘ β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
Assertion
Ref Expression
dchrval (πœ‘ β†’ 𝐺 = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
Distinct variable groups:   π‘₯,𝐡   π‘₯,𝑁   π‘₯,π‘ˆ   πœ‘,π‘₯   π‘₯,𝑍
Allowed substitution hints:   𝐷(π‘₯)   𝐺(π‘₯)
Proof of Theorem dchrval
Dummy variables 𝑧 𝑛 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrval.g . 2 𝐺 = (DChrβ€˜π‘)
2 df-dchr 26736 . . 3 DChr = (𝑛 ∈ β„• ↦ ⦋(β„€/nβ„€β€˜π‘›) / π‘§β¦Œβ¦‹{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩})
3 fvexd 6907 . . . 4 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) ∈ V)
4 ovex 7442 . . . . . . 7 ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∈ V
54rabex 5333 . . . . . 6 {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} ∈ V
65a1i 11 . . . . 5 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} ∈ V)
7 dchrval.d . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
87ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
9 dchrval.z . . . . . . . . . . . . . . . 16 𝑍 = (β„€/nβ„€β€˜π‘)
10 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ 𝑛 = 𝑁)
1110fveq2d 6896 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) = (β„€/nβ„€β€˜π‘))
129, 11eqtr4id 2792 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ 𝑍 = (β„€/nβ„€β€˜π‘›))
1312eqeq2d 2744 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (𝑧 = 𝑍 ↔ 𝑧 = (β„€/nβ„€β€˜π‘›)))
1413biimpar 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝑧 = 𝑍)
1514fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (mulGrpβ€˜π‘§) = (mulGrpβ€˜π‘))
1615oveq1d 7424 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) = ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)))
1714fveq2d 6896 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = (Baseβ€˜π‘))
18 dchrval.b . . . . . . . . . . . . . . 15 𝐡 = (Baseβ€˜π‘)
1917, 18eqtr4di 2791 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = 𝐡)
2014fveq2d 6896 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = (Unitβ€˜π‘))
21 dchrval.u . . . . . . . . . . . . . . 15 π‘ˆ = (Unitβ€˜π‘)
2220, 21eqtr4di 2791 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = π‘ˆ)
2319, 22difeq12d 4124 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) = (𝐡 βˆ– π‘ˆ))
2423xpeq1d 5706 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) = ((𝐡 βˆ– π‘ˆ) Γ— {0}))
2524sseq1d 4014 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯ ↔ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯))
2616, 25rabeqbidv 3450 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
278, 26eqtr4d 2776 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯})
2827eqeq2d 2744 . . . . . . . 8 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (𝑏 = 𝐷 ↔ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}))
2928biimpar 479 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ 𝑏 = 𝐷)
3029opeq2d 4881 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(Baseβ€˜ndx), π‘βŸ© = ⟨(Baseβ€˜ndx), 𝐷⟩)
3129sqxpeqd 5709 . . . . . . . 8 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ (𝑏 Γ— 𝑏) = (𝐷 Γ— 𝐷))
3231reseq2d 5982 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏)) = ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷)))
3332opeq2d 4881 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩ = ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩)
3430, 33preq12d 4746 . . . . 5 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
356, 34csbied 3932 . . . 4 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ⦋{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
363, 35csbied 3932 . . 3 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ ⦋(β„€/nβ„€β€˜π‘›) / π‘§β¦Œβ¦‹{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
37 dchrval.n . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
38 prex 5433 . . . 4 {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V
3938a1i 11 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V)
402, 36, 37, 39fvmptd2 7007 . 2 (πœ‘ β†’ (DChrβ€˜π‘) = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
411, 40eqtrid 2785 1 (πœ‘ β†’ 𝐺 = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3433  Vcvv 3475  β¦‹csb 3894   βˆ– cdif 3946   βŠ† wss 3949  {csn 4629  {cpr 4631  βŸ¨cop 4635   Γ— cxp 5675   β†Ύ cres 5679  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668  0cc0 11110   Β· cmul 11115  β„•cn 12212  ndxcnx 17126  Basecbs 17144  +gcplusg 17197   MndHom cmhm 18669  mulGrpcmgp 19987  Unitcui 20169  β„‚fldccnfld 20944  β„€/nβ„€czn 21052  DChrcdchr 26735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-res 5689  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-dchr 26736
This theorem is referenced by:  dchrbas  26738  dchrplusg  26750
  Copyright terms: Public domain W3C validator