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