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

Metamath Proof Explorer

Theorem dchreq

Proof