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 · 𝑋 ) = 𝑋 )