Theorem dchrbas

Description: Base set 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	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrbas.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	dchrbas	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )

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		dchrbas.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
7		eqidd	⊢ ( 𝜑 → { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
8	1 2 3 4 5 7	dchrval	⊢ ( 𝜑 → 𝐺 = { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ } )
9	8	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ } ) )
10		ovex	⊢ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∈ V
11	10	rabex	⊢ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ∈ V
12		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ }
13	12	grpbase	⊢ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ∈ V → { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ } ) )
14	11 13	ax-mp	⊢ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } × { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) ⟩ } )
15	9 6 14	3eqtr4g	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )