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 syl5eq
 |-  ( ( 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 syl5eq
 |-  ( ( 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 ) )