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