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 ( 𝜑 → ( ( 𝑋𝑈 ) = ( 𝑌𝑈 ) ↔ 𝑋 = 𝑌 ) )