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

Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝐺 )
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 = ( 0g ‘ 𝐺 )
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 dchrmullid ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 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 sselid ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑍 ) )
27 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
28 20 24 26 27 fvmptd ⊢ ( 𝜑 → ( 1 ‘ 𝐴 ) = 1 )