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

Metamath Proof Explorer

Theorem dchrresb

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 ⊢ G = DChr ⁡ N
dchrresb.z ⊢ Z = ℤ/Nℤ
dchrresb.b ⊢ D = Base G
dchrresb.u ⊢ U = Unit ⁡ Z
dchrresb.x ⊢ φ → X ∈ D
dchrresb.Y ⊢ φ → Y ∈ D
Assertion dchrresb ⊢ φ → X ↾ U = Y ↾ U ↔ X = Y

Proof

Step Hyp Ref Expression
1 dchrresb.g ⊢ G = DChr ⁡ N
2 dchrresb.z ⊢ Z = ℤ/Nℤ
3 dchrresb.b ⊢ D = Base G
4 dchrresb.u ⊢ U = Unit ⁡ Z
5 dchrresb.x ⊢ φ → X ∈ D
6 dchrresb.Y ⊢ φ → Y ∈ D
7 eqid ⊢ Base Z = Base Z
8 1 2 3 7 5 dchrf ⊢ φ → X : Base Z ⟶ ℂ
9 8 ffnd ⊢ φ → X Fn Base Z
10 1 2 3 7 6 dchrf ⊢ φ → Y : Base Z ⟶ ℂ
11 10 ffnd ⊢ φ → Y Fn Base Z
12 7 4 unitss ⊢ U ⊆ Base Z
13 fvreseq ⊢ X Fn Base Z ∧ Y Fn Base Z ∧ U ⊆ Base Z → X ↾ U = Y ↾ U ↔ ∀ k ∈ U X ⁡ k = Y ⁡ k
14 12 13 mpan2 ⊢ X Fn Base Z ∧ Y Fn Base Z → X ↾ U = Y ↾ U ↔ ∀ k ∈ U X ⁡ k = Y ⁡ k
15 9 11 14 syl2anc ⊢ φ → X ↾ U = Y ↾ U ↔ ∀ k ∈ U X ⁡ k = Y ⁡ k
16 1 2 3 4 5 6 dchreq ⊢ φ → X = Y ↔ ∀ k ∈ U X ⁡ k = Y ⁡ k
17 15 16 bitr4d ⊢ φ → X ↾ U = Y ↾ U ↔ X = Y