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 · 𝑌 ) )