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

Metamath Proof Explorer

Theorem dchrmul

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 ‘ 𝐺 )
dchrmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion dchrmul ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 ∘f · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrmul.t ⊢ · = ( +g ‘ 𝐺 )
5 dchrmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 dchrmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
7 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
8 5 7 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 1 2 3 4 8 dchrplusg ⊢ ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )
10 9 oveqd ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 𝑌 ) )
11 5 6 ofmresval ⊢ ( 𝜑 → ( 𝑋 ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 𝑌 ) = ( 𝑋 ∘f · 𝑌 ) )
12 10 11 eqtrd ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 ∘f · 𝑌 ) )