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

Metamath Proof Explorer

Theorem dchrmullid

Description: Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrn0.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrn0.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchr1cl.o ⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
dchrmullid.t ⊢ · = ( +g ‘ 𝐺 )
dchrmullid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion dchrmullid ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrn0.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchrn0.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
6 dchr1cl.o ⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
7 dchrmullid.t ⊢ · = ( +g ‘ 𝐺 )
8 dchrmullid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
10 8 9 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
11 1 2 3 4 5 6 10 dchr1cl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
12 1 2 3 7 11 8 dchrmul ⊢ ( 𝜑 → ( 1 · 𝑋 ) = ( 1 ∘f · 𝑋 ) )
13 oveq1 ⊢ ( 1 = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) → ( 1 · ( 𝑋 ‘ 𝑘 ) ) = ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) )
14 13 eqeq1d ⊢ ( 1 = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) → ( ( 1 · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) ↔ ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) ) )
15 oveq1 ⊢ ( 0 = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) → ( 0 · ( 𝑋 ‘ 𝑘 ) ) = ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) )
16 15 eqeq1d ⊢ ( 0 = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) → ( ( 0 · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) ↔ ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) ) )
17 1 2 3 4 8 dchrf ⊢ ( 𝜑 → 𝑋 : 𝐵 ⟶ ℂ )
18 17 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
20 19 mullidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → ( 1 · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) )
21 0cn ⊢ 0 ∈ ℂ
22 21 mul02i ⊢ ( 0 · 0 ) = 0
23 1 2 4 5 10 3 dchrelbas2 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑘 ∈ 𝐵 ( ( 𝑋 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) ) ) )
24 8 23 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑘 ∈ 𝐵 ( ( 𝑋 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) ) )
25 24 simprd ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐵 ( ( 𝑋 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) )
26 25 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) )
27 26 necon1bd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ¬ 𝑘 ∈ 𝑈 → ( 𝑋 ‘ 𝑘 ) = 0 ) )
28 27 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ ¬ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) = 0 )
29 28 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ ¬ 𝑘 ∈ 𝑈 ) → ( 0 · ( 𝑋 ‘ 𝑘 ) ) = ( 0 · 0 ) )
30 22 29 28 3eqtr4a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ ¬ 𝑘 ∈ 𝑈 ) → ( 0 · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) )
31 14 16 20 30 ifbothda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) = ( 𝑋 ‘ 𝑘 ) )
32 31 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐵 ↦ ( 𝑋 ‘ 𝑘 ) ) )
33 4 fvexi ⊢ 𝐵 ∈ V
34 33 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
35 ax-1cn ⊢ 1 ∈ ℂ
36 35 21 ifcli ⊢ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ∈ ℂ
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ∈ ℂ )
38 6 a1i ⊢ ( 𝜑 → 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) )
39 17 feqmptd ⊢ ( 𝜑 → 𝑋 = ( 𝑘 ∈ 𝐵 ↦ ( 𝑋 ‘ 𝑘 ) ) )
40 34 37 18 38 39 offval2 ⊢ ( 𝜑 → ( 1 ∘f · 𝑋 ) = ( 𝑘 ∈ 𝐵 ↦ ( if ( 𝑘 ∈ 𝑈 , 1 , 0 ) · ( 𝑋 ‘ 𝑘 ) ) ) )
41 32 40 39 3eqtr4d ⊢ ( 𝜑 → ( 1 ∘f · 𝑋 ) = 𝑋 )
42 12 41 eqtrd ⊢ ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )