Metamath Proof Explorer

Theorem lgsqrlem3

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses lgsqr.y 
|- Y = ( Z/nZ ` P )
lgsqr.s 
|- S = ( Poly1 ` Y )
lgsqr.b 
|- B = ( Base ` S )
lgsqr.d 
|- D = ( deg1 ` Y )
lgsqr.o 
|- O = ( eval1 ` Y )
lgsqr.e 
|- .^ = ( .g ` ( mulGrp ` S ) )
lgsqr.x 
|- X = ( var1 ` Y )
lgsqr.m 
|- .- = ( -g ` S )
lgsqr.u 
|- .1. = ( 1r ` S )
lgsqr.t 
|- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )
lgsqr.l 
|- L = ( ZRHom ` Y )
lgsqr.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgsqr.g 
|- G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )
lgsqr.3 
|- ( ph -> A e. ZZ )
lgsqr.4 
|- ( ph -> ( A /L P ) = 1 )
Assertion lgsqrlem3 
|- ( ph -> ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )

Proof

Step Hyp Ref Expression
1 lgsqr.y 
 |-  Y = ( Z/nZ ` P )
2 lgsqr.s 
 |-  S = ( Poly1 ` Y )
3 lgsqr.b 
 |-  B = ( Base ` S )
4 lgsqr.d 
 |-  D = ( deg1 ` Y )
5 lgsqr.o 
 |-  O = ( eval1 ` Y )
6 lgsqr.e 
 |-  .^ = ( .g ` ( mulGrp ` S ) )
7 lgsqr.x 
 |-  X = ( var1 ` Y )
8 lgsqr.m 
 |-  .- = ( -g ` S )
9 lgsqr.u 
 |-  .1. = ( 1r ` S )
10 lgsqr.t 
 |-  T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )
11 lgsqr.l 
 |-  L = ( ZRHom ` Y )
12 lgsqr.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
13 lgsqr.g 
 |-  G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )
14 lgsqr.3 
 |-  ( ph -> A e. ZZ )
15 lgsqr.4 
 |-  ( ph -> ( A /L P ) = 1 )
16 12 eldifad 
 |-  ( ph -> P e. Prime )
17 1 znfld 
 |-  ( P e. Prime -> Y e. Field )
18 16 17 syl 
 |-  ( ph -> Y e. Field )
19 fldidom 
 |-  ( Y e. Field -> Y e. IDomn )
20 18 19 syl 
 |-  ( ph -> Y e. IDomn )
21 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
22 21 simplbi 
 |-  ( Y e. IDomn -> Y e. CRing )
23 20 22 syl 
 |-  ( ph -> Y e. CRing )
24 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
25 23 24 syl 
 |-  ( ph -> Y e. Ring )
26 11 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
27 25 26 syl 
 |-  ( ph -> L e. ( ZZring RingHom Y ) )
28 zringbas 
 |-  ZZ = ( Base ` ZZring )
29 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
30 28 29 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
31 27 30 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
32 31 14 ffvelcdmd 
 |-  ( ph -> ( L ` A ) e. ( Base ` Y ) )
33 lgsvalmod 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )
34 14 12 33 syl2anc 
 |-  ( ph -> ( ( A /L P ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )
35 15 oveq1d 
 |-  ( ph -> ( ( A /L P ) mod P ) = ( 1 mod P ) )
36 34 35 eqtr3d 
 |-  ( ph -> ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 14 36 lgsqrlem1 
 |-  ( ph -> ( ( O ` T ) ` ( L ` A ) ) = ( 0g ` Y ) )
38 eqid 
 |-  ( Y ^s ( Base ` Y ) ) = ( Y ^s ( Base ` Y ) )
39 eqid 
 |-  ( Base ` ( Y ^s ( Base ` Y ) ) ) = ( Base ` ( Y ^s ( Base ` Y ) ) )
40 fvexd 
 |-  ( ph -> ( Base ` Y ) e. _V )
41 5 2 38 29 evl1rhm 
 |-  ( Y e. CRing -> O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) )
42 23 41 syl 
 |-  ( ph -> O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) )
43 3 39 rhmf 
 |-  ( O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) -> O : B --> ( Base ` ( Y ^s ( Base ` Y ) ) ) )
44 42 43 syl 
 |-  ( ph -> O : B --> ( Base ` ( Y ^s ( Base ` Y ) ) ) )
45 2 ply1ring 
 |-  ( Y e. Ring -> S e. Ring )
46 25 45 syl 
 |-  ( ph -> S e. Ring )
47 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
48 46 47 syl 
 |-  ( ph -> S e. Grp )
49 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
50 49 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
51 49 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
52 46 51 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
53 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
54 12 53 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
55 54 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
56 7 2 3 vr1cl 
 |-  ( Y e. Ring -> X e. B )
57 25 56 syl 
 |-  ( ph -> X e. B )
58 50 6 52 55 57 mulgnn0cld 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
59 3 9 ringidcl 
 |-  ( S e. Ring -> .1. e. B )
60 46 59 syl 
 |-  ( ph -> .1. e. B )
61 3 8 grpsubcl 
 |-  ( ( S e. Grp /\ ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ .1. e. B ) -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
62 48 58 60 61 syl3anc 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
63 10 62 eqeltrid 
 |-  ( ph -> T e. B )
64 44 63 ffvelcdmd 
 |-  ( ph -> ( O ` T ) e. ( Base ` ( Y ^s ( Base ` Y ) ) ) )
65 38 29 39 18 40 64 pwselbas 
 |-  ( ph -> ( O ` T ) : ( Base ` Y ) --> ( Base ` Y ) )
66 65 ffnd 
 |-  ( ph -> ( O ` T ) Fn ( Base ` Y ) )
67 fniniseg 
 |-  ( ( O ` T ) Fn ( Base ` Y ) -> ( ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> ( ( L ` A ) e. ( Base ` Y ) /\ ( ( O ` T ) ` ( L ` A ) ) = ( 0g ` Y ) ) ) )
68 66 67 syl 
 |-  ( ph -> ( ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> ( ( L ` A ) e. ( Base ` Y ) /\ ( ( O ` T ) ` ( L ` A ) ) = ( 0g ` Y ) ) ) )
69 32 37 68 mpbir2and 
 |-  ( ph -> ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )