Metamath Proof Explorer

Theorem lgsqrlem1

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 } ) )
lgsqrlem1.3 
|- ( ph -> A e. ZZ )
lgsqrlem1.4 
|- ( ph -> ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) )
Assertion lgsqrlem1 
|- ( ph -> ( ( O ` T ) ` ( L ` A ) ) = ( 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 lgsqrlem1.3 
 |-  ( ph -> A e. ZZ )
14 lgsqrlem1.4 
 |-  ( ph -> ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) )
15 10 fveq2i 
 |-  ( O ` T ) = ( O ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) )
16 15 fveq1i 
 |-  ( ( O ` T ) ` ( L ` A ) ) = ( ( O ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) ) ` ( L ` A ) )
17 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
18 12 eldifad 
 |-  ( ph -> P e. Prime )
19 1 znfld 
 |-  ( P e. Prime -> Y e. Field )
20 18 19 syl 
 |-  ( ph -> Y e. Field )
21 fldidom 
 |-  ( Y e. Field -> Y e. IDomn )
22 20 21 syl 
 |-  ( ph -> Y e. IDomn )
23 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
24 23 simplbi 
 |-  ( Y e. IDomn -> Y e. CRing )
25 22 24 syl 
 |-  ( ph -> Y e. CRing )
26 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
27 25 26 syl 
 |-  ( ph -> Y e. Ring )
28 11 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
29 27 28 syl 
 |-  ( ph -> L e. ( ZZring RingHom Y ) )
30 zringbas 
 |-  ZZ = ( Base ` ZZring )
31 30 17 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
32 29 31 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
33 32 13 ffvelrnd 
 |-  ( ph -> ( L ` A ) e. ( Base ` Y ) )
34 5 7 17 2 3 25 33 evl1vard 
 |-  ( ph -> ( X e. B /\ ( ( O ` X ) ` ( L ` A ) ) = ( L ` A ) ) )
35 eqid 
 |-  ( .g ` ( mulGrp ` Y ) ) = ( .g ` ( mulGrp ` Y ) )
36 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
37 12 36 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
38 37 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
39 5 2 17 3 25 33 34 6 35 38 evl1expd 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) ) )
40 zringmpg 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )
41 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
42 40 41 rhmmhm 
 |-  ( L e. ( ZZring RingHom Y ) -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Y ) ) )
43 29 42 syl 
 |-  ( ph -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Y ) ) )
44 40 30 mgpbas 
 |-  ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
45 eqid 
 |-  ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
46 44 45 35 mhmmulg 
 |-  ( ( L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Y ) ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ A e. ZZ ) -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) )
47 43 38 13 46 syl3anc 
 |-  ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) )
48 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
49 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
50 49 subrgsubm 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
51 48 50 mp1i 
 |-  ( ph -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
52 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
53 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( ( mulGrp ` CCfld ) |`s ZZ )
54 52 53 45 submmulg 
 |-  ( ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ A e. ZZ ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) )
55 51 38 13 54 syl3anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) )
56 13 zcnd 
 |-  ( ph -> A e. CC )
57 cnfldexp 
 |-  ( ( A e. CC /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
58 56 38 57 syl2anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
59 55 58 eqtr3d 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
60 59 fveq2d 
 |-  ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) ) = ( L ` ( A ^ ( ( P - 1 ) / 2 ) ) ) )
61 prmnn 
 |-  ( P e. Prime -> P e. NN )
62 18 61 syl 
 |-  ( ph -> P e. NN )
63 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
64 13 38 63 syl2anc 
 |-  ( ph -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
65 1zzd 
 |-  ( ph -> 1 e. ZZ )
66 moddvds 
 |-  ( ( P e. NN /\ ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) <-> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
67 62 64 65 66 syl3anc 
 |-  ( ph -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) <-> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
68 14 67 mpbid 
 |-  ( ph -> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) )
69 62 nnnn0d 
 |-  ( ph -> P e. NN0 )
70 1 11 zndvds 
 |-  ( ( P e. NN0 /\ ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( L ` ( A ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` 1 ) <-> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
71 69 64 65 70 syl3anc 
 |-  ( ph -> ( ( L ` ( A ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` 1 ) <-> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
72 68 71 mpbird 
 |-  ( ph -> ( L ` ( A ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` 1 ) )
73 zring1 
 |-  1 = ( 1r ` ZZring )
74 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
75 73 74 rhm1 
 |-  ( L e. ( ZZring RingHom Y ) -> ( L ` 1 ) = ( 1r ` Y ) )
76 29 75 syl 
 |-  ( ph -> ( L ` 1 ) = ( 1r ` Y ) )
77 60 72 76 3eqtrd 
 |-  ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) A ) ) = ( 1r ` Y ) )
78 47 77 eqtr3d 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) = ( 1r ` Y ) )
79 78 eqeq2d 
 |-  ( ph -> ( ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) <-> ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( 1r ` Y ) ) )
80 79 anbi2d 
 |-  ( ph -> ( ( ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` Y ) ) ( L ` A ) ) ) <-> ( ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( 1r ` Y ) ) ) )
81 39 80 mpbid 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ ( ( O ` ( ( ( P - 1 ) / 2 ) .^ X ) ) ` ( L ` A ) ) = ( 1r ` Y ) ) )
82 eqid 
 |-  ( algSc ` S ) = ( algSc ` S )
83 17 74 ringidcl 
 |-  ( Y e. Ring -> ( 1r ` Y ) e. ( Base ` Y ) )
84 27 83 syl 
 |-  ( ph -> ( 1r ` Y ) e. ( Base ` Y ) )
85 5 2 17 82 3 25 84 33 evl1scad 
 |-  ( ph -> ( ( ( algSc ` S ) ` ( 1r ` Y ) ) e. B /\ ( ( O ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) ` ( L ` A ) ) = ( 1r ` Y ) ) )
86 2 82 74 9 ply1scl1 
 |-  ( Y e. Ring -> ( ( algSc ` S ) ` ( 1r ` Y ) ) = .1. )
87 27 86 syl 
 |-  ( ph -> ( ( algSc ` S ) ` ( 1r ` Y ) ) = .1. )
88 87 eleq1d 
 |-  ( ph -> ( ( ( algSc ` S ) ` ( 1r ` Y ) ) e. B <-> .1. e. B ) )
89 87 fveq2d 
 |-  ( ph -> ( O ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) = ( O ` .1. ) )
90 89 fveq1d 
 |-  ( ph -> ( ( O ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) ` ( L ` A ) ) = ( ( O ` .1. ) ` ( L ` A ) ) )
91 90 eqeq1d 
 |-  ( ph -> ( ( ( O ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) ` ( L ` A ) ) = ( 1r ` Y ) <-> ( ( O ` .1. ) ` ( L ` A ) ) = ( 1r ` Y ) ) )
92 88 91 anbi12d 
 |-  ( ph -> ( ( ( ( algSc ` S ) ` ( 1r ` Y ) ) e. B /\ ( ( O ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) ` ( L ` A ) ) = ( 1r ` Y ) ) <-> ( .1. e. B /\ ( ( O ` .1. ) ` ( L ` A ) ) = ( 1r ` Y ) ) ) )
93 85 92 mpbid 
 |-  ( ph -> ( .1. e. B /\ ( ( O ` .1. ) ` ( L ` A ) ) = ( 1r ` Y ) ) )
94 eqid 
 |-  ( -g ` Y ) = ( -g ` Y )
95 5 2 17 3 25 33 81 93 8 94 evl1subd 
 |-  ( ph -> ( ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B /\ ( ( O ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) ) ` ( L ` A ) ) = ( ( 1r ` Y ) ( -g ` Y ) ( 1r ` Y ) ) ) )
96 95 simprd 
 |-  ( ph -> ( ( O ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) ) ` ( L ` A ) ) = ( ( 1r ` Y ) ( -g ` Y ) ( 1r ` Y ) ) )
97 16 96 syl5eq 
 |-  ( ph -> ( ( O ` T ) ` ( L ` A ) ) = ( ( 1r ` Y ) ( -g ` Y ) ( 1r ` Y ) ) )
98 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
99 27 98 syl 
 |-  ( ph -> Y e. Grp )
100 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
101 17 100 94 grpsubid 
 |-  ( ( Y e. Grp /\ ( 1r ` Y ) e. ( Base ` Y ) ) -> ( ( 1r ` Y ) ( -g ` Y ) ( 1r ` Y ) ) = ( 0g ` Y ) )
102 99 84 101 syl2anc 
 |-  ( ph -> ( ( 1r ` Y ) ( -g ` Y ) ( 1r ` Y ) ) = ( 0g ` Y ) )
103 97 102 eqtrd 
 |-  ( ph -> ( ( O ` T ) ` ( L ` A ) ) = ( 0g ` Y ) )