Theorem dchrzrhmul

Description: A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrelbas4.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	dchrzrh1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrzrh1.a	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	dchrzrh1.c	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
Assertion	dchrzrhmul	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrelbas4.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
5		dchrzrh1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6		dchrzrh1.a	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
7		dchrzrh1.c	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
8	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
9	5 8	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10	9	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11	2	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
12	10 11	syl	⊢ ( 𝜑 → 𝑍 ∈ CRing )
13		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
14	12 13	syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
15	4	zrhrhm	⊢ ( 𝑍 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
16	14 15	syl	⊢ ( 𝜑 → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
17		zringbas	⊢ ℤ = ( Base ‘ ℤring )
18		zringmulr	⊢ · = ( .r ‘ ℤring )
19		eqid	⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
20	17 18 19	rhmmul	⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) = ( ( 𝐿 ‘ 𝐴 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝐶 ) ) )
21	16 6 7 20	syl3anc	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) = ( ( 𝐿 ‘ 𝐴 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝐶 ) ) )
22	21	fveq2d	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) ) = ( 𝑋 ‘ ( ( 𝐿 ‘ 𝐴 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝐶 ) ) ) )
23	1 2 3	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
24	23 5	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
25		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
26	17 25	rhmf	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
27	16 26	syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
28	27 6	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑍 ) )
29	27 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐶 ) ∈ ( Base ‘ 𝑍 ) )
30		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
31	30 25	mgpbas	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
32	30 19	mgpplusg	⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
33		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
34		cnfldmul	⊢ · = ( .r ‘ ℂfld )
35	33 34	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
36	31 32 35	mhmlin	⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑍 ) ∧ ( 𝐿 ‘ 𝐶 ) ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝐴 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝐶 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝐶 ) ) ) )
37	24 28 29 36	syl3anc	⊢ ( 𝜑 → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝐴 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝐶 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝐶 ) ) ) )
38	22 37	eqtrd	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝐶 ) ) ) )