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 · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )