Metamath Proof Explorer


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 𝑁 ) )