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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrresb.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrresb.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrresb.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrresb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrresb.Y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion dchrresb ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) = ( 𝑌 ↾ 𝑈 ) ↔ 𝑋 = 𝑌 ) )

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 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
8 1 2 3 7 5 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
9 8 ffnd ⊢ ( 𝜑 → 𝑋 Fn ( Base ‘ 𝑍 ) )
10 1 2 3 7 6 dchrf ⊢ ( 𝜑 → 𝑌 : ( Base ‘ 𝑍 ) ⟶ ℂ )
11 10 ffnd ⊢ ( 𝜑 → 𝑌 Fn ( Base ‘ 𝑍 ) )
12 7 4 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
13 fvreseq ⊢ ( ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) ∧ 𝑈 ⊆ ( Base ‘ 𝑍 ) ) → ( ( 𝑋 ↾ 𝑈 ) = ( 𝑌 ↾ 𝑈 ) ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
14 12 13 mpan2 ⊢ ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) → ( ( 𝑋 ↾ 𝑈 ) = ( 𝑌 ↾ 𝑈 ) ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
15 9 11 14 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) = ( 𝑌 ↾ 𝑈 ) ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
16 1 2 3 4 5 6 dchreq ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑘 ) ) )
17 15 16 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) = ( 𝑌 ↾ 𝑈 ) ↔ 𝑋 = 𝑌 ) )