This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrval

Description: Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrval.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrval.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrval.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dchrval.d ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
Assertion dchrval ( 𝜑 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )

Proof

Step Hyp Ref Expression
1 dchrval.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrval.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrval.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
4 dchrval.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 dchrval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 dchrval.d ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
7 df-dchr ⊢ DChr = ( 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )
8 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ( ℤ/nℤ ‘ 𝑛 ) ∈ V )
9 ovex ⊢ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∈ V
10 9 rabex ⊢ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ∈ V
11 10 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ∈ V )
12 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
14 13 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ( ℤ/nℤ ‘ 𝑛 ) = ( ℤ/nℤ ‘ 𝑁 ) )
15 2 14 eqtr4id ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → 𝑍 = ( ℤ/nℤ ‘ 𝑛 ) )
16 15 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ( 𝑧 = 𝑍 ↔ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) )
17 16 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → 𝑧 = 𝑍 )
18 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( mulGrp ‘ 𝑧 ) = ( mulGrp ‘ 𝑍 ) )
19 18 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) = ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
20 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑍 ) )
21 20 3 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( Base ‘ 𝑧 ) = 𝐵 )
22 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( Unit ‘ 𝑧 ) = ( Unit ‘ 𝑍 ) )
23 22 4 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( Unit ‘ 𝑧 ) = 𝑈 )
24 21 23 difeq12d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) = ( 𝐵 ∖ 𝑈 ) )
25 24 xpeq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) )
26 25 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 ↔ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 ) )
27 19 26 rabeqbidv ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
28 12 27 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } )
29 28 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ( 𝑏 = 𝐷 ↔ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) )
30 29 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → 𝑏 = 𝐷 )
31 30 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ )
32 30 sqxpeqd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → ( 𝑏 × 𝑏 ) = ( 𝐷 × 𝐷 ) )
33 32 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )
34 33 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ )
35 31 34 preq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) ∧ 𝑏 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
36 11 35 csbied ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑁 ) ∧ 𝑧 = ( ℤ/nℤ ‘ 𝑛 ) ) → ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
37 8 36 csbied ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
38 prex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ∈ V
39 38 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ∈ V )
40 7 37 5 39 fvmptd2 ⊢ ( 𝜑 → ( DChr ‘ 𝑁 ) = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
41 1 40 eqtrid ⊢ ( 𝜑 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )