MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrval Structured version   Visualization version   GIF version

Theorem dchrval 26598
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 26597 . . 3 DChr = (𝑛 ∈ β„• ↦ ⦋(β„€/nβ„€β€˜π‘›) / π‘§β¦Œβ¦‹{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩})
3 fvexd 6862 . . . 4 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) ∈ V)
4 ovex 7395 . . . . . . 7 ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∈ V
54rabex 5294 . . . . . 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 6851 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) = (β„€/nβ„€β€˜π‘))
129, 11eqtr4id 2796 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ 𝑍 = (β„€/nβ„€β€˜π‘›))
1312eqeq2d 2748 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (𝑧 = 𝑍 ↔ 𝑧 = (β„€/nβ„€β€˜π‘›)))
1413biimpar 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝑧 = 𝑍)
1514fveq2d 6851 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (mulGrpβ€˜π‘§) = (mulGrpβ€˜π‘))
1615oveq1d 7377 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) = ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)))
1714fveq2d 6851 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = (Baseβ€˜π‘))
18 dchrval.b . . . . . . . . . . . . . . 15 𝐡 = (Baseβ€˜π‘)
1917, 18eqtr4di 2795 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = 𝐡)
2014fveq2d 6851 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = (Unitβ€˜π‘))
21 dchrval.u . . . . . . . . . . . . . . 15 π‘ˆ = (Unitβ€˜π‘)
2220, 21eqtr4di 2795 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = π‘ˆ)
2319, 22difeq12d 4088 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) = (𝐡 βˆ– π‘ˆ))
2423xpeq1d 5667 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) = ((𝐡 βˆ– π‘ˆ) Γ— {0}))
2524sseq1d 3980 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯ ↔ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯))
2616, 25rabeqbidv 3427 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
278, 26eqtr4d 2780 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯})
2827eqeq2d 2748 . . . . . . . 8 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (𝑏 = 𝐷 ↔ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}))
2928biimpar 479 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ 𝑏 = 𝐷)
3029opeq2d 4842 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(Baseβ€˜ndx), π‘βŸ© = ⟨(Baseβ€˜ndx), 𝐷⟩)
3129sqxpeqd 5670 . . . . . . . 8 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ (𝑏 Γ— 𝑏) = (𝐷 Γ— 𝐷))
3231reseq2d 5942 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏)) = ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷)))
3332opeq2d 4842 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩ = ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩)
3430, 33preq12d 4707 . . . . 5 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
356, 34csbied 3898 . . . 4 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ⦋{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
363, 35csbied 3898 . . 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 5394 . . . 4 {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V
3938a1i 11 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V)
402, 36, 37, 39fvmptd2 6961 . 2 (πœ‘ β†’ (DChrβ€˜π‘) = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
411, 40eqtrid 2789 1 (πœ‘ β†’ 𝐺 = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3410  Vcvv 3448  β¦‹csb 3860   βˆ– cdif 3912   βŠ† wss 3915  {csn 4591  {cpr 4593  βŸ¨cop 4597   Γ— cxp 5636   β†Ύ cres 5640  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620  0cc0 11058   Β· cmul 11063  β„•cn 12160  ndxcnx 17072  Basecbs 17090  +gcplusg 17140   MndHom cmhm 18606  mulGrpcmgp 19903  Unitcui 20075  β„‚fldccnfld 20812  β„€/nβ„€czn 20919  DChrcdchr 26596
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 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-res 5650  df-iota 6453  df-fun 6503  df-fv 6509  df-ov 7365  df-dchr 26597
This theorem is referenced by:  dchrbas  26599  dchrplusg  26611
  Copyright terms: Public domain W3C validator