Theorem lgsdchrval

Description: The Legendre symbol function X ( m ) = ( m /L N ) , where N is an odd positive number, is a Dirichlet character modulo N . (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	lgsdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	lgsdchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	lgsdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	lgsdchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	lgsdchr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	lgsdchr.x	⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
Assertion	lgsdchrval	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 𝐴 /L 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		lgsdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		lgsdchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		lgsdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		lgsdchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		lgsdchr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
6		lgsdchr.x	⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
7		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8	7	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ0 )
9	2 4 5	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 )
10		fof	⊢ ( 𝐿 : ℤ –onto→ 𝐵 → 𝐿 : ℤ ⟶ 𝐵 )
11	8 9 10	3syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝐿 : ℤ ⟶ 𝐵 )
12	11	ffvelrnda	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) ∈ 𝐵 )
13		eqeq1	⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ↔ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) )
14	13	anbi1d	⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
15	14	rexbidv	⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
16	15	iotabidv	⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
17		iotaex	⊢ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V
18	16 6 17	fvmpt3i	⊢ ( ( 𝐿 ‘ 𝐴 ) ∈ 𝐵 → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
19	12 18	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
20		ovex	⊢ ( 𝐴 /L 𝑁 ) ∈ V
21		simprr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) )
22		simplll	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ )
23	22 7	syl	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ0 )
24		simplr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝐴 ∈ ℤ )
25		simprl	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑚 ∈ ℤ )
26	2 5	zndvds	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) )
27	23 24 25 26	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) )
28	21 27	mpbid	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∥ ( 𝐴 − 𝑚 ) )
29		moddvds	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) )
30	22 24 25 29	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) )
31	28 30	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) )
32	31	oveq1d	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) )
33		simpllr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ¬ 2 ∥ 𝑁 )
34		lgsmod	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )
35	24 22 33 34	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )
36		lgsmod	⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) = ( 𝑚 /L 𝑁 ) )
37	25 22 33 36	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) = ( 𝑚 /L 𝑁 ) )
38	32 35 37	3eqtr3d	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐴 /L 𝑁 ) = ( 𝑚 /L 𝑁 ) )
39	38	eqeq2d	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ℎ = ( 𝐴 /L 𝑁 ) ↔ ℎ = ( 𝑚 /L 𝑁 ) ) )
40	39	biimprd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ℎ = ( 𝑚 /L 𝑁 ) → ℎ = ( 𝐴 /L 𝑁 ) ) )
41	40	anassrs	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) → ( ℎ = ( 𝑚 /L 𝑁 ) → ℎ = ( 𝐴 /L 𝑁 ) ) )
42	41	expimpd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) → ℎ = ( 𝐴 /L 𝑁 ) ) )
43	42	rexlimdva	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) → ℎ = ( 𝐴 /L 𝑁 ) ) )
44		fveq2	⊢ ( 𝑚 = 𝐴 → ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝐴 ) )
45	44	eqcomd	⊢ ( 𝑚 = 𝐴 → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) )
46	45	biantrurd	⊢ ( 𝑚 = 𝐴 → ( ℎ = ( 𝑚 /L 𝑁 ) ↔ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
47		oveq1	⊢ ( 𝑚 = 𝐴 → ( 𝑚 /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )
48	47	eqeq2d	⊢ ( 𝑚 = 𝐴 → ( ℎ = ( 𝑚 /L 𝑁 ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) )
49	46 48	bitr3d	⊢ ( 𝑚 = 𝐴 → ( ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) )
50	49	rspcev	⊢ ( ( 𝐴 ∈ ℤ ∧ ℎ = ( 𝐴 /L 𝑁 ) ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) )
51	50	ex	⊢ ( 𝐴 ∈ ℤ → ( ℎ = ( 𝐴 /L 𝑁 ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
52	51	adantl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ℎ = ( 𝐴 /L 𝑁 ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
53	43 52	impbid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) )
54	53	adantr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 /L 𝑁 ) ∈ V ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) )
55	54	iota5	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 /L 𝑁 ) ∈ V ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( 𝐴 /L 𝑁 ) )
56	20 55	mpan2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( 𝐴 /L 𝑁 ) )
57	19 56	eqtrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 𝐴 /L 𝑁 ) )