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