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

Metamath Proof Explorer

Theorem dchrzrh1

Description: Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016)

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

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 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
7 5 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 7 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
10 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
11 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
12 4 11 zrh1 ⊢ ( 𝑍 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
13 8 9 10 12 4syl ⊢ ( 𝜑 → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
14 13 fveq2d ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
15 1 2 3 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
16 15 5 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
17 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
18 17 11 ringidval ⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
19 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
20 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
21 19 20 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
22 18 21 mhm0 ⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
23 16 22 syl ⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
24 14 23 eqtrd ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )