dchr1

Description: Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchr1.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchr1.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchr1.o	⊢ 1 = ( 0_g ‘ 𝐺 )
	dchr1.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchr1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchr1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	dchr1	⊢ ( 𝜑 → ( 1 ‘ 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		dchr1.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchr1.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchr1.o	⊢ 1 = ( 0_g ‘ 𝐺 )
4		dchr1.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
5		dchr1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		dchr1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
9		eqid	⊢ ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
10	1 2 7 8 4 9 5	dchr1cl	⊢ ( 𝜑 → ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ∈ ( Base ‘ 𝐺 ) )
11		eleq1w	⊢ ( 𝑘 = 𝑥 → ( 𝑘 ∈ 𝑈 ↔ 𝑥 ∈ 𝑈 ) )
12	11	ifbid	⊢ ( 𝑘 = 𝑥 → if ( 𝑘 ∈ 𝑈 , 1 , 0 ) = if ( 𝑥 ∈ 𝑈 , 1 , 0 ) )
13	12	cbvmptv	⊢ ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑥 ∈ 𝑈 , 1 , 0 ) )
14		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
15	1 2 7 8 4 13 14 10	dchrmulid2	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ( +_g ‘ 𝐺 ) ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) )
16	1	dchrabl	⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
17		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
18	7 14 3	isgrpid2	⊢ ( 𝐺 ∈ Grp → ( ( ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ∈ ( Base ‘ 𝐺 ) ∧ ( ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ( +_g ‘ 𝐺 ) ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) ↔ 1 = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) )
19	5 16 17 18	4syl	⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ∈ ( Base ‘ 𝐺 ) ∧ ( ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ( +_g ‘ 𝐺 ) ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) ↔ 1 = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ) )
20	10 15 19	mpbi2and	⊢ ( 𝜑 → 1 = ( 𝑘 ∈ ( Base ‘ 𝑍 ) ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝑘 = 𝐴 )
22	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐴 ∈ 𝑈 )
23	21 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝑘 ∈ 𝑈 )
24	23	iftrued	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → if ( 𝑘 ∈ 𝑈 , 1 , 0 ) = 1 )
25	8 4	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
26	25 6	sseldi	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑍 ) )
27		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
28	20 24 26 27	fvmptd	⊢ ( 𝜑 → ( 1 ‘ 𝐴 ) = 1 )

Metamath Proof Explorer

Theorem dchr1

Proof