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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝐶 ) ) ) )