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

Metamath Proof Explorer

Theorem dchreq

Description: A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrresb.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrresb.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrresb.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrresb.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrresb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrresb.Y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion dchreq ( 𝜑 → ( 𝑋 = 𝑌 ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 dchrresb.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrresb.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrresb.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrresb.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 dchrresb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 dchrresb.Y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
7 eldif ⊢ ( 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ↔ ( 𝑘 ∈ ( Base ‘ 𝑍 ) ∧ ¬ 𝑘 ∈ 𝑈 ) )
8 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → 𝑋 ∈ 𝐷 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → 𝑘 ∈ ( Base ‘ 𝑍 ) )
11 1 2 3 8 4 9 10 dchrn0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ∈ 𝑈 ) )
12 11 biimpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) )
13 12 necon1bd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ¬ 𝑘 ∈ 𝑈 → ( 𝑋 ‘ 𝑘 ) = 0 ) )
14 13 impr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑍 ) ∧ ¬ 𝑘 ∈ 𝑈 ) ) → ( 𝑋 ‘ 𝑘 ) = 0 )
15 7 14 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) → ( 𝑋 ‘ 𝑘 ) = 0 )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → 𝑌 ∈ 𝐷 )
17 1 2 3 8 4 16 10 dchrn0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑌 ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ∈ 𝑈 ) )
18 17 biimpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑌 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ 𝑈 ) )
19 18 necon1bd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( ¬ 𝑘 ∈ 𝑈 → ( 𝑌 ‘ 𝑘 ) = 0 ) )
20 19 impr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑍 ) ∧ ¬ 𝑘 ∈ 𝑈 ) ) → ( 𝑌 ‘ 𝑘 ) = 0 )
21 7 20 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) → ( 𝑌 ‘ 𝑘 ) = 0 )
22 15 21 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) → ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) )
24 1 2 3 8 5 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
25 24 ffnd ⊢ ( 𝜑 → 𝑋 Fn ( Base ‘ 𝑍 ) )
26 1 2 3 8 6 dchrf ⊢ ( 𝜑 → 𝑌 : ( Base ‘ 𝑍 ) ⟶ ℂ )
27 26 ffnd ⊢ ( 𝜑 → 𝑌 Fn ( Base ‘ 𝑍 ) )
28 eqfnfv ⊢ ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
29 25 27 28 syl2anc ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ∀ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
30 8 4 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
31 undif ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑍 ) ↔ ( 𝑈 ∪ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) = ( Base ‘ 𝑍 ) )
32 30 31 mpbi ⊢ ( 𝑈 ∪ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) = ( Base ‘ 𝑍 )
33 32 raleqi ⊢ ( ∀ 𝑘 ∈ ( 𝑈 ∪ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) )
34 ralunb ⊢ ( ∀ 𝑘 ∈ ( 𝑈 ∪ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ↔ ( ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ∧ ∀ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
35 33 34 bitr3i ⊢ ( ∀ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ↔ ( ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ∧ ∀ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
36 29 35 bitrdi ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ( ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ∧ ∀ 𝑘 ∈ ( ( Base ‘ 𝑍 ) ∖ 𝑈 ) ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) ) )
37 23 36 mpbiran2d ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )