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

Metamath Proof Explorer

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 } ) ⊆ 𝑥 } )