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 
|- G = ( DChr ` N )
lgsdchr.z 
|- Z = ( Z/nZ ` N )
lgsdchr.d 
|- D = ( Base ` G )
lgsdchr.b 
|- B = ( Base ` Z )
lgsdchr.l 
|- L = ( ZRHom ` Z )
lgsdchr.x 
|- X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) )
Assertion lgsdchrval 
|- ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( X ` ( L ` A ) ) = ( A /L N ) )

Proof

Step Hyp Ref Expression
1 lgsdchr.g 
 |-  G = ( DChr ` N )
2 lgsdchr.z 
 |-  Z = ( Z/nZ ` N )
3 lgsdchr.d 
 |-  D = ( Base ` G )
4 lgsdchr.b 
 |-  B = ( Base ` Z )
5 lgsdchr.l 
 |-  L = ( ZRHom ` Z )
6 lgsdchr.x 
 |-  X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) )
7 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
8 7 adantr 
 |-  ( ( N e. NN /\ -. 2 || N ) -> N e. NN0 )
9 2 4 5 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> B )
10 fof 
 |-  ( L : ZZ -onto-> B -> L : ZZ --> B )
11 8 9 10 3syl 
 |-  ( ( N e. NN /\ -. 2 || N ) -> L : ZZ --> B )
12 11 ffvelcdmda 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( L ` A ) e. B )
13 eqeq1 
 |-  ( y = ( L ` A ) -> ( y = ( L ` m ) <-> ( L ` A ) = ( L ` m ) ) )
14 13 anbi1d 
 |-  ( y = ( L ` A ) -> ( ( y = ( L ` m ) /\ h = ( m /L N ) ) <-> ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
15 14 rexbidv 
 |-  ( y = ( L ` A ) -> ( E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) <-> E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
16 15 iotabidv 
 |-  ( y = ( L ` A ) -> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) = ( iota h E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
17 iotaex 
 |-  ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) e. _V
18 16 6 17 fvmpt3i 
 |-  ( ( L ` A ) e. B -> ( X ` ( L ` A ) ) = ( iota h E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
19 12 18 syl 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( X ` ( L ` A ) ) = ( iota h E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
20 ovex 
 |-  ( A /L N ) e. _V
21 simprr 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( L ` A ) = ( L ` m ) )
22 simplll 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> N e. NN )
23 22 7 syl 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> N e. NN0 )
24 simplr 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> A e. ZZ )
25 simprl 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> m e. ZZ )
26 2 5 zndvds 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ m e. ZZ ) -> ( ( L ` A ) = ( L ` m ) <-> N || ( A - m ) ) )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( ( L ` A ) = ( L ` m ) <-> N || ( A - m ) ) )
28 21 27 mpbid 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> N || ( A - m ) )
29 moddvds 
 |-  ( ( N e. NN /\ A e. ZZ /\ m e. ZZ ) -> ( ( A mod N ) = ( m mod N ) <-> N || ( A - m ) ) )
30 22 24 25 29 syl3anc 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( ( A mod N ) = ( m mod N ) <-> N || ( A - m ) ) )
31 28 30 mpbird 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( A mod N ) = ( m mod N ) )
32 31 oveq1d 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( ( A mod N ) /L N ) = ( ( m mod N ) /L N ) )
33 simpllr 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> -. 2 || N )
34 lgsmod 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( A /L N ) )
35 24 22 33 34 syl3anc 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( ( A mod N ) /L N ) = ( A /L N ) )
36 lgsmod 
 |-  ( ( m e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( m mod N ) /L N ) = ( m /L N ) )
37 25 22 33 36 syl3anc 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( ( m mod N ) /L N ) = ( m /L N ) )
38 32 35 37 3eqtr3d 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( A /L N ) = ( m /L N ) )
39 38 eqeq2d 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( h = ( A /L N ) <-> h = ( m /L N ) ) )
40 39 biimprd 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( m e. ZZ /\ ( L ` A ) = ( L ` m ) ) ) -> ( h = ( m /L N ) -> h = ( A /L N ) ) )
41 40 anassrs 
 |-  ( ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ m e. ZZ ) /\ ( L ` A ) = ( L ` m ) ) -> ( h = ( m /L N ) -> h = ( A /L N ) ) )
42 41 expimpd 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ m e. ZZ ) -> ( ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) -> h = ( A /L N ) ) )
43 42 rexlimdva 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) -> h = ( A /L N ) ) )
44 fveq2 
 |-  ( m = A -> ( L ` m ) = ( L ` A ) )
45 44 eqcomd 
 |-  ( m = A -> ( L ` A ) = ( L ` m ) )
46 45 biantrurd 
 |-  ( m = A -> ( h = ( m /L N ) <-> ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
47 oveq1 
 |-  ( m = A -> ( m /L N ) = ( A /L N ) )
48 47 eqeq2d 
 |-  ( m = A -> ( h = ( m /L N ) <-> h = ( A /L N ) ) )
49 46 48 bitr3d 
 |-  ( m = A -> ( ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) <-> h = ( A /L N ) ) )
50 49 rspcev 
 |-  ( ( A e. ZZ /\ h = ( A /L N ) ) -> E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) )
51 50 ex 
 |-  ( A e. ZZ -> ( h = ( A /L N ) -> E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
52 51 adantl 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( h = ( A /L N ) -> E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) )
53 43 52 impbid 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) <-> h = ( A /L N ) ) )
54 53 adantr 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( A /L N ) e. _V ) -> ( E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) <-> h = ( A /L N ) ) )
55 54 iota5 
 |-  ( ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) /\ ( A /L N ) e. _V ) -> ( iota h E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) = ( A /L N ) )
56 20 55 mpan2 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( iota h E. m e. ZZ ( ( L ` A ) = ( L ` m ) /\ h = ( m /L N ) ) ) = ( A /L N ) )
57 19 56 eqtrd 
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( X ` ( L ` A ) ) = ( A /L N ) )