Metamath Proof Explorer

Theorem lgseisenlem4

Description: Lemma for lgseisen . The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015) (Proof shortened by AV, 15-Jun-2019)

Ref Expression
Hypotheses lgseisen.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2 
|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3 
|- ( ph -> P =/= Q )
lgseisen.4 
|- R = ( ( Q x. ( 2 x. x ) ) mod P )
lgseisen.5 
|- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
lgseisen.6 
|- S = ( ( Q x. ( 2 x. y ) ) mod P )
lgseisen.7 
|- Y = ( Z/nZ ` P )
lgseisen.8 
|- G = ( mulGrp ` Y )
lgseisen.9 
|- L = ( ZRHom ` Y )
Assertion lgseisenlem4 
|- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 lgseisen.2 
 |-  ( ph -> Q e. ( Prime \ { 2 } ) )
3 lgseisen.3 
 |-  ( ph -> P =/= Q )
4 lgseisen.4 
 |-  R = ( ( Q x. ( 2 x. x ) ) mod P )
5 lgseisen.5 
 |-  M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
6 lgseisen.6 
 |-  S = ( ( Q x. ( 2 x. y ) ) mod P )
7 lgseisen.7 
 |-  Y = ( Z/nZ ` P )
8 lgseisen.8 
 |-  G = ( mulGrp ` Y )
9 lgseisen.9 
 |-  L = ( ZRHom ` Y )
10 zringbas 
 |-  ZZ = ( Base ` ZZring )
11 zring0 
 |-  0 = ( 0g ` ZZring )
12 zringabl 
 |-  ZZring e. Abel
13 ablcmn 
 |-  ( ZZring e. Abel -> ZZring e. CMnd )
14 12 13 mp1i 
 |-  ( ph -> ZZring e. CMnd )
15 1 eldifad 
 |-  ( ph -> P e. Prime )
16 7 znfld 
 |-  ( P e. Prime -> Y e. Field )
17 15 16 syl 
 |-  ( ph -> Y e. Field )
18 isfld 
 |-  ( Y e. Field <-> ( Y e. DivRing /\ Y e. CRing ) )
19 18 simprbi 
 |-  ( Y e. Field -> Y e. CRing )
20 17 19 syl 
 |-  ( ph -> Y e. CRing )
21 8 crngmgp 
 |-  ( Y e. CRing -> G e. CMnd )
22 20 21 syl 
 |-  ( ph -> G e. CMnd )
23 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
24 22 23 syl 
 |-  ( ph -> G e. Mnd )
25 fzfid 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin )
26 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
27 20 26 syl 
 |-  ( ph -> Y e. Ring )
28 9 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
29 27 28 syl 
 |-  ( ph -> L e. ( ZZring RingHom Y ) )
30 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
31 10 30 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
32 29 31 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
33 m1expcl 
 |-  ( k e. ZZ -> ( -u 1 ^ k ) e. ZZ )
34 33 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> ( -u 1 ^ k ) e. ZZ )
35 32 34 cofmpt 
 |-  ( ph -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) = ( k e. ZZ |-> ( L ` ( -u 1 ^ k ) ) ) )
36 zringmpg 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )
37 36 8 rhmmhm 
 |-  ( L e. ( ZZring RingHom Y ) -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) )
38 29 37 syl 
 |-  ( ph -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) )
39 neg1cn 
 |-  -u 1 e. CC
40 neg1ne0 
 |-  -u 1 =/= 0
41 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
42 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
43 41 42 expghm 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
44 39 40 43 mp2an 
 |-  ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
45 ghmmhm 
 |-  ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
46 44 45 ax-mp 
 |-  ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
47 cnring 
 |-  CCfld e. Ring
48 cnfldbas 
 |-  CC = ( Base ` CCfld )
49 cnfld0 
 |-  0 = ( 0g ` CCfld )
50 cndrng 
 |-  CCfld e. DivRing
51 48 49 50 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
52 51 41 unitsubm 
 |-  ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
53 47 52 ax-mp 
 |-  ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) )
54 42 resmhm2 
 |-  ( ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) )
55 46 53 54 mp2an 
 |-  ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) )
56 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
57 41 subrgsubm 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
58 56 57 ax-mp 
 |-  ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) )
59 34 fmpttd 
 |-  ( ph -> ( k e. ZZ |-> ( -u 1 ^ k ) ) : ZZ --> ZZ )
60 59 frnd 
 |-  ( ph -> ran ( k e. ZZ |-> ( -u 1 ^ k ) ) C_ ZZ )
61 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( ( mulGrp ` CCfld ) |`s ZZ )
62 61 resmhm2b 
 |-  ( ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ran ( k e. ZZ |-> ( -u 1 ^ k ) ) C_ ZZ ) -> ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) <-> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) )
63 58 60 62 sylancr 
 |-  ( ph -> ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) <-> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) )
64 55 63 mpbii 
 |-  ( ph -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) )
65 mhmco 
 |-  ( ( L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) /\ ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) )
66 38 64 65 syl2anc 
 |-  ( ph -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) )
67 35 66 eqeltrrd 
 |-  ( ph -> ( k e. ZZ |-> ( L ` ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) )
68 2 gausslemma2dlem0a 
 |-  ( ph -> Q e. NN )
69 68 nnred 
 |-  ( ph -> Q e. RR )
70 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
71 69 70 nndivred 
 |-  ( ph -> ( Q / P ) e. RR )
72 71 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q / P ) e. RR )
73 2nn 
 |-  2 e. NN
74 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
75 74 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN )
76 nnmulcl 
 |-  ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
77 73 75 76 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. NN )
78 77 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. RR )
79 72 78 remulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q / P ) x. ( 2 x. x ) ) e. RR )
80 79 flcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ )
81 eqid 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) )
82 fvexd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. _V )
83 c0ex 
 |-  0 e. _V
84 83 a1i 
 |-  ( ph -> 0 e. _V )
85 81 25 82 84 fsuppmptdm 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) finSupp 0 )
86 oveq2 
 |-  ( k = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
87 86 fveq2d 
 |-  ( k = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) -> ( L ` ( -u 1 ^ k ) ) = ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
88 oveq2 
 |-  ( k = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
89 88 fveq2d 
 |-  ( k = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) -> ( L ` ( -u 1 ^ k ) ) = ( L ` ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) )
90 10 11 14 24 25 67 80 85 87 89 gsummhm2 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) = ( L ` ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) )
91 8 30 mgpbas 
 |-  ( Base ` Y ) = ( Base ` G )
92 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
93 8 92 mgpplusg 
 |-  ( .r ` Y ) = ( +g ` G )
94 32 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L : ZZ --> ( Base ` Y ) )
95 m1expcl 
 |-  ( ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ )
96 80 95 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ )
97 94 96 ffvelrnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) e. ( Base ` Y ) )
98 neg1z 
 |-  -u 1 e. ZZ
99 2 eldifad 
 |-  ( ph -> Q e. Prime )
100 99 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. Prime )
101 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
102 100 101 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ZZ )
103 77 nnzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ZZ )
104 102 103 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
105 15 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime )
106 prmnn 
 |-  ( P e. Prime -> P e. NN )
107 105 106 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
108 104 107 zmodcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 )
109 4 108 eqeltrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN0 )
110 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ R e. NN0 ) -> ( -u 1 ^ R ) e. ZZ )
111 98 109 110 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. ZZ )
112 111 102 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. Q ) e. ZZ )
113 94 112 ffvelrnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ R ) x. Q ) ) e. ( Base ` Y ) )
114 eqid 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
115 eqid 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) )
116 91 93 22 25 97 113 114 115 gsummptfidmadd2 
 |-  ( ph -> ( G gsum ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) = ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) )
117 eqidd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
118 eqidd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) )
119 25 97 113 117 118 offval2 
 |-  ( ph -> ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ( .r ` Y ) ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) )
120 29 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L e. ( ZZring RingHom Y ) )
121 zringmulr 
 |-  x. = ( .r ` ZZring )
122 10 121 92 rhmmul 
 |-  ( ( L e. ( ZZring RingHom Y ) /\ ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ /\ ( ( -u 1 ^ R ) x. Q ) e. ZZ ) -> ( L ` ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) ) = ( ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ( .r ` Y ) ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) )
123 120 96 112 122 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) ) = ( ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ( .r ` Y ) ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) )
124 104 zred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR )
125 107 nnrpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR+ )
126 modval 
 |-  ( ( ( Q x. ( 2 x. x ) ) e. RR /\ P e. RR+ ) -> ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) ) )
127 124 125 126 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) ) )
128 4 127 eqtrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) ) )
129 102 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. CC )
130 77 nncnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. CC )
131 107 nncnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. CC )
132 107 nnne0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P =/= 0 )
133 129 130 131 132 div23d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) / P ) = ( ( Q / P ) x. ( 2 x. x ) ) )
134 133 fveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) )
135 134 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) = ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
136 135 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) ) = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
137 128 136 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
138 137 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) = ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
139 prmz 
 |-  ( P e. Prime -> P e. ZZ )
140 105 139 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ )
141 140 80 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ )
142 141 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC )
143 104 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. CC )
144 142 143 pncan3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) = ( Q x. ( 2 x. x ) ) )
145 2cnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. CC )
146 75 nncnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. CC )
147 129 145 146 mul12d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) = ( 2 x. ( Q x. x ) ) )
148 138 144 147 3eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) = ( 2 x. ( Q x. x ) ) )
149 148 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) ) = ( -u 1 ^ ( 2 x. ( Q x. x ) ) ) )
150 39 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 e. CC )
151 40 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 =/= 0 )
152 109 nn0zd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ZZ )
153 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ /\ R e. ZZ ) ) -> ( -u 1 ^ ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) ) = ( ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) x. ( -u 1 ^ R ) ) )
154 150 151 141 152 153 syl22anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) ) = ( ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) x. ( -u 1 ^ R ) ) )
155 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( P e. ZZ /\ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ ) ) -> ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ( -u 1 ^ P ) ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
156 150 151 140 80 155 syl22anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ( -u 1 ^ P ) ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
157 1cnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 e. CC )
158 eldifsni 
 |-  ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
159 1 158 syl 
 |-  ( ph -> P =/= 2 )
160 159 necomd 
 |-  ( ph -> 2 =/= P )
161 160 neneqd 
 |-  ( ph -> -. 2 = P )
162 161 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. 2 = P )
163 2z 
 |-  2 e. ZZ
164 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
165 163 164 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
166 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) )
167 165 105 166 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 || P <-> 2 = P ) )
168 162 167 mtbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. 2 || P )
169 oexpneg 
 |-  ( ( 1 e. CC /\ P e. NN /\ -. 2 || P ) -> ( -u 1 ^ P ) = -u ( 1 ^ P ) )
170 157 107 168 169 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ P ) = -u ( 1 ^ P ) )
171 1exp 
 |-  ( P e. ZZ -> ( 1 ^ P ) = 1 )
172 140 171 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 ^ P ) = 1 )
173 172 negeqd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u ( 1 ^ P ) = -u 1 )
174 170 173 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ P ) = -u 1 )
175 174 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ P ) ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
176 156 175 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
177 176 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) x. ( -u 1 ^ R ) ) = ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) )
178 154 177 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) ) = ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) )
179 nnmulcl 
 |-  ( ( Q e. NN /\ x e. NN ) -> ( Q x. x ) e. NN )
180 68 74 179 syl2an 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. NN )
181 180 nnnn0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. NN0 )
182 2nn0 
 |-  2 e. NN0
183 182 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. NN0 )
184 150 181 183 expmuld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( 2 x. ( Q x. x ) ) ) = ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) )
185 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
186 185 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) = ( 1 ^ ( Q x. x ) )
187 180 nnzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. ZZ )
188 1exp 
 |-  ( ( Q x. x ) e. ZZ -> ( 1 ^ ( Q x. x ) ) = 1 )
189 187 188 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 ^ ( Q x. x ) ) = 1 )
190 186 189 eqtrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) = 1 )
191 184 190 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( 2 x. ( Q x. x ) ) ) = 1 )
192 149 178 191 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) = 1 )
193 192 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) x. Q ) = ( 1 x. Q ) )
194 96 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC )
195 111 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. CC )
196 194 195 129 mulassd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) x. Q ) = ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) )
197 129 mulid2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. Q ) = Q )
198 193 196 197 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) = Q )
199 198 fveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) ) = ( L ` Q ) )
200 123 199 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ( .r ` Y ) ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) = ( L ` Q ) )
201 200 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ( .r ` Y ) ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) )
202 119 201 eqtrd 
 |-  ( ph -> ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) )
203 202 oveq2d 
 |-  ( ph -> ( G gsum ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) )
204 1 2 3 4 5 6 7 8 9 lgseisenlem3 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) )
205 204 oveq2d 
 |-  ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) = ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) )
206 116 203 205 3eqtr3rd 
 |-  ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) )
207 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
208 97 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( Base ` Y ) )
209 fvexd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) e. _V )
210 fvexd 
 |-  ( ph -> ( 0g ` G ) e. _V )
211 114 25 209 210 fsuppmptdm 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) finSupp ( 0g ` G ) )
212 91 207 22 25 208 211 gsumcl 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) e. ( Base ` Y ) )
213 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
214 30 92 213 ringridm 
 |-  ( ( Y e. Ring /\ ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) )
215 27 212 214 syl2anc 
 |-  ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) )
216 99 101 syl 
 |-  ( ph -> Q e. ZZ )
217 32 216 ffvelrnd 
 |-  ( ph -> ( L ` Q ) e. ( Base ` Y ) )
218 eqid 
 |-  ( .g ` G ) = ( .g ` G )
219 91 218 gsumconst 
 |-  ( ( G e. Mnd /\ ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin /\ ( L ` Q ) e. ( Base ` Y ) ) -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) )
220 24 25 217 219 syl3anc 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) )
221 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
222 1 221 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
223 222 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
224 hashfz1 
 |-  ( ( ( P - 1 ) / 2 ) e. NN0 -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) )
225 223 224 syl 
 |-  ( ph -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) )
226 225 oveq1d 
 |-  ( ph -> ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) )
227 36 10 mgpbas 
 |-  ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
228 eqid 
 |-  ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
229 227 228 218 mhmmulg 
 |-  ( ( L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ Q e. ZZ ) -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) )
230 38 223 216 229 syl3anc 
 |-  ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) )
231 58 a1i 
 |-  ( ph -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
232 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
233 232 61 228 submmulg 
 |-  ( ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ Q e. ZZ ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) )
234 231 223 216 233 syl3anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) )
235 216 zcnd 
 |-  ( ph -> Q e. CC )
236 cnfldexp 
 |-  ( ( Q e. CC /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) )
237 235 223 236 syl2anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) )
238 234 237 eqtr3d 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) )
239 238 fveq2d 
 |-  ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) )
240 230 239 eqtr3d 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) )
241 220 226 240 3eqtrd 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) )
242 206 215 241 3eqtr3d 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) )
243 subrgsubg 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
244 56 243 ax-mp 
 |-  ZZ e. ( SubGrp ` CCfld )
245 subgsubm 
 |-  ( ZZ e. ( SubGrp ` CCfld ) -> ZZ e. ( SubMnd ` CCfld ) )
246 244 245 mp1i 
 |-  ( ph -> ZZ e. ( SubMnd ` CCfld ) )
247 80 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ZZ )
248 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
249 25 246 247 248 gsumsubm 
 |-  ( ph -> ( CCfld gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
250 80 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. CC )
251 25 250 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) )
252 249 251 eqtr3d 
 |-  ( ph -> ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) )
253 252 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
254 253 fveq2d 
 |-  ( ph -> ( L ` ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) = ( L ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
255 90 242 254 3eqtr3d 
 |-  ( ph -> ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
256 70 nnnn0d 
 |-  ( ph -> P e. NN0 )
257 zexpcl 
 |-  ( ( Q e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
258 216 223 257 syl2anc 
 |-  ( ph -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
259 25 80 fsumzcl 
 |-  ( ph -> sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ )
260 m1expcl 
 |-  ( sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ )
261 259 260 syl 
 |-  ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ )
262 7 9 zndvds 
 |-  ( ( P e. NN0 /\ ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) -> ( ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) <-> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
263 256 258 261 262 syl3anc 
 |-  ( ph -> ( ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) <-> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
264 255 263 mpbid 
 |-  ( ph -> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) )
265 moddvds 
 |-  ( ( P e. NN /\ ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) -> ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) <-> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
266 70 258 261 265 syl3anc 
 |-  ( ph -> ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) <-> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) )
267 264 266 mpbird 
 |-  ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) )