MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrval Structured version   Visualization version   GIF version
Theorem dchrval 26973
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 26972 . . 3 DChr = (𝑛 ∈ β„• ↦ ⦋(β„€/nβ„€β€˜π‘›) / π‘§β¦Œβ¦‹{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩})
3 fvexd 6905 . . . 4 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) ∈ V)
4 ovex 7444 . . . . . . 7 ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∈ V
54rabex 5331 . . . . . 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 722 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
9 dchrval.z . . . . . . . . . . . . . . . 16 𝑍 = (β„€/nβ„€β€˜π‘)
10 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ 𝑛 = 𝑁)
1110fveq2d 6894 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (β„€/nβ„€β€˜π‘›) = (β„€/nβ„€β€˜π‘))
129, 11eqtr4id 2789 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ 𝑍 = (β„€/nβ„€β€˜π‘›))
1312eqeq2d 2741 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 = 𝑁) β†’ (𝑧 = 𝑍 ↔ 𝑧 = (β„€/nβ„€β€˜π‘›)))
1413biimpar 476 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝑧 = 𝑍)
1514fveq2d 6894 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (mulGrpβ€˜π‘§) = (mulGrpβ€˜π‘))
1615oveq1d 7426 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) = ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)))
1714fveq2d 6894 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = (Baseβ€˜π‘))
18 dchrval.b . . . . . . . . . . . . . . 15 𝐡 = (Baseβ€˜π‘)
1917, 18eqtr4di 2788 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Baseβ€˜π‘§) = 𝐡)
2014fveq2d 6894 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = (Unitβ€˜π‘))
21 dchrval.u . . . . . . . . . . . . . . 15 π‘ˆ = (Unitβ€˜π‘)
2220, 21eqtr4di 2788 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (Unitβ€˜π‘§) = π‘ˆ)
2319, 22difeq12d 4122 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) = (𝐡 βˆ– π‘ˆ))
2423xpeq1d 5704 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) = ((𝐡 βˆ– π‘ˆ) Γ— {0}))
2524sseq1d 4012 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ((((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯ ↔ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯))
2616, 25rabeqbidv 3447 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} = {π‘₯ ∈ ((mulGrpβ€˜π‘) MndHom (mulGrpβ€˜β„‚fld)) ∣ ((𝐡 βˆ– π‘ˆ) Γ— {0}) βŠ† π‘₯})
278, 26eqtr4d 2773 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ 𝐷 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯})
2827eqeq2d 2741 . . . . . . . 8 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ (𝑏 = 𝐷 ↔ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}))
2928biimpar 476 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ 𝑏 = 𝐷)
3029opeq2d 4879 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(Baseβ€˜ndx), π‘βŸ© = ⟨(Baseβ€˜ndx), 𝐷⟩)
3129sqxpeqd 5707 . . . . . . . 8 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ (𝑏 Γ— 𝑏) = (𝐷 Γ— 𝐷))
3231reseq2d 5980 . . . . . . 7 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏)) = ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷)))
3332opeq2d 4879 . . . . . 6 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩ = ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩)
3430, 33preq12d 4744 . . . . 5 ((((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) ∧ 𝑏 = {π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯}) β†’ {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
356, 34csbied 3930 . . . 4 (((πœ‘ ∧ 𝑛 = 𝑁) ∧ 𝑧 = (β„€/nβ„€β€˜π‘›)) β†’ ⦋{π‘₯ ∈ ((mulGrpβ€˜π‘§) MndHom (mulGrpβ€˜β„‚fld)) ∣ (((Baseβ€˜π‘§) βˆ– (Unitβ€˜π‘§)) Γ— {0}) βŠ† π‘₯} / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝑏 Γ— 𝑏))⟩} = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
363, 35csbied 3930 . . 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 5431 . . . 4 {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V
3938a1i 11 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩} ∈ V)
402, 36, 37, 39fvmptd2 7005 . 2 (πœ‘ β†’ (DChrβ€˜π‘) = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
411, 40eqtrid 2782 1 (πœ‘ β†’ 𝐺 = {⟨(Baseβ€˜ndx), 𝐷⟩, ⟨(+gβ€˜ndx), ( ∘f Β· β†Ύ (𝐷 Γ— 𝐷))⟩})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  {crab 3430  Vcvv 3472  β¦‹csb 3892   βˆ– cdif 3944   βŠ† wss 3947  {csn 4627  {cpr 4629  βŸ¨cop 4633   Γ— cxp 5673   β†Ύ cres 5677  β€˜cfv 6542  (class class class)co 7411   ∘f cof 7670  0cc0 11112   Β· cmul 11117  β„•cn 12216  ndxcnx 17130  Basecbs 17148  +gcplusg 17201   MndHom cmhm 18703  mulGrpcmgp 20028  Unitcui 20246  β„‚fldccnfld 21144  β„€/nβ„€czn 21271  DChrcdchr 26971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-res 5687  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7414  df-dchr 26972
This theorem is referenced by:  dchrbas  26974  dchrplusg  26986
  Copyright terms: Public domain W3C validator