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

Metamath Proof Explorer

Theorem dchrplusg

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

Ref Expression
Hypotheses dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrmul.t ⊢ · = ( +g ‘ 𝐺 )
dchrplusg.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion dchrplusg ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrmul.t ⊢ · = ( +g ‘ 𝐺 )
5 dchrplusg.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
7 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
8 1 2 6 7 5 3 dchrbas ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 } )
9 1 2 6 7 5 8 dchrval ⊢ ( 𝜑 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
10 9 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ) )
11 3 fvexi ⊢ 𝐷 ∈ V
12 11 11 xpex ⊢ ( 𝐷 × 𝐷 ) ∈ V
13 ofexg ⊢ ( ( 𝐷 × 𝐷 ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V )
14 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ }
15 14 grpplusg ⊢ ( ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ) )
16 12 13 15 mp2b ⊢ ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
17 10 4 16 3eqtr4g ⊢ ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )