Metamath Proof Explorer

Theorem lgseisenlem3

Description: Lemma for lgseisen . (Contributed by Mario Carneiro, 17-Jun-2015) (Proof shortened by AV, 28-Jul-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 lgseisenlem3 
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) )

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 oveq2 
 |-  ( k = x -> ( 2 x. k ) = ( 2 x. x ) )
11 10 fveq2d 
 |-  ( k = x -> ( L ` ( 2 x. k ) ) = ( L ` ( 2 x. x ) ) )
12 11 cbvmptv 
 |-  ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) )
13 12 oveq2i 
 |-  ( G gsum ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) )
14 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
15 8 14 mgpbas 
 |-  ( Base ` Y ) = ( Base ` G )
16 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
17 1 eldifad 
 |-  ( ph -> P e. Prime )
18 7 znfld 
 |-  ( P e. Prime -> Y e. Field )
19 17 18 syl 
 |-  ( ph -> Y e. Field )
20 isfld 
 |-  ( Y e. Field <-> ( Y e. DivRing /\ Y e. CRing ) )
21 20 simprbi 
 |-  ( Y e. Field -> Y e. CRing )
22 19 21 syl 
 |-  ( ph -> Y e. CRing )
23 8 crngmgp 
 |-  ( Y e. CRing -> G e. CMnd )
24 22 23 syl 
 |-  ( ph -> G e. CMnd )
25 fzfid 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin )
26 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
27 22 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 zringbas 
 |-  ZZ = ( Base ` ZZring )
31 30 14 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
32 29 31 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
33 2z 
 |-  2 e. ZZ
34 elfzelz 
 |-  ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> k e. ZZ )
35 zmulcl 
 |-  ( ( 2 e. ZZ /\ k e. ZZ ) -> ( 2 x. k ) e. ZZ )
36 33 34 35 sylancr 
 |-  ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( 2 x. k ) e. ZZ )
37 ffvelcdm 
 |-  ( ( L : ZZ --> ( Base ` Y ) /\ ( 2 x. k ) e. ZZ ) -> ( L ` ( 2 x. k ) ) e. ( Base ` Y ) )
38 32 36 37 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. k ) ) e. ( Base ` Y ) )
39 38 fmpttd 
 |-  ( ph -> ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( Base ` Y ) )
40 eqid 
 |-  ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) = ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) )
41 fvexd 
 |-  ( ( ph /\ k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. k ) ) e. _V )
42 fvexd 
 |-  ( ph -> ( 0g ` G ) e. _V )
43 40 25 41 42 fsuppmptdm 
 |-  ( ph -> ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) finSupp ( 0g ` G ) )
44 1 2 3 4 5 6 lgseisenlem2 
 |-  ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
45 15 16 24 25 39 43 44 gsumf1o 
 |-  ( ph -> ( G gsum ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) ) = ( G gsum ( ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) o. M ) ) )
46 13 45 eqtr3id 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) = ( G gsum ( ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) o. M ) ) )
47 1 2 3 4 5 lgseisenlem1 
 |-  ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
48 5 fmpt 
 |-  ( A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
49 47 48 sylibr 
 |-  ( ph -> A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
50 5 a1i 
 |-  ( ph -> M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) )
51 eqidd 
 |-  ( ph -> ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) = ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) )
52 oveq2 
 |-  ( k = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) -> ( 2 x. k ) = ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) )
53 52 fveq2d 
 |-  ( k = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) -> ( L ` ( 2 x. k ) ) = ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) )
54 49 50 51 53 fmptcof 
 |-  ( ph -> ( ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) o. M ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) ) )
55 54 oveq2d 
 |-  ( ph -> ( G gsum ( ( k e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. k ) ) ) o. M ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) ) ) )
56 2 eldifad 
 |-  ( ph -> Q e. Prime )
57 56 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. Prime )
58 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
59 57 58 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ZZ )
60 2nn 
 |-  2 e. NN
61 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
62 61 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN )
63 nnmulcl 
 |-  ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
64 60 62 63 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. NN )
65 64 nnzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ZZ )
66 59 65 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
67 17 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime )
68 prmnn 
 |-  ( P e. Prime -> P e. NN )
69 67 68 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
70 66 69 zmodcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 )
71 4 70 eqeltrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN0 )
72 71 nn0zd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ZZ )
73 m1expcl 
 |-  ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ )
74 72 73 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. ZZ )
75 74 72 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
76 75 69 zmodcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
77 76 nn0cnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. CC )
78 2cnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. CC )
79 2ne0 
 |-  2 =/= 0
80 79 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 =/= 0 )
81 77 78 80 divcan2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) )
82 81 fveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) = ( L ` ( ( ( -u 1 ^ R ) x. R ) mod P ) ) )
83 69 nnrpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR+ )
84 eqidd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) mod P ) = ( ( -u 1 ^ R ) mod P ) )
85 4 oveq1i 
 |-  ( R mod P ) = ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P )
86 66 zred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR )
87 modabs2 
 |-  ( ( ( Q x. ( 2 x. x ) ) e. RR /\ P e. RR+ ) -> ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
88 86 83 87 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
89 85 88 eqtrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
90 74 74 72 66 83 84 89 modmul12d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) )
91 75 zred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. RR )
92 modabs2 
 |-  ( ( ( ( -u 1 ^ R ) x. R ) e. RR /\ P e. RR+ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) )
93 91 83 92 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) )
94 74 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. CC )
95 59 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. CC )
96 65 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. CC )
97 94 95 96 mulassd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) = ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) )
98 97 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) )
99 90 93 98 3eqtr4d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) mod P ) = ( ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) mod P ) )
100 17 68 syl 
 |-  ( ph -> P e. NN )
101 100 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
102 76 nn0zd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ZZ )
103 74 59 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. Q ) e. ZZ )
104 103 65 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) e. ZZ )
105 moddvds 
 |-  ( ( P e. NN /\ ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ZZ /\ ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) e. ZZ ) -> ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) mod P ) = ( ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) mod P ) <-> P || ( ( ( ( -u 1 ^ R ) x. R ) mod P ) - ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) ) )
106 101 102 104 105 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) mod P ) = ( ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) mod P ) <-> P || ( ( ( ( -u 1 ^ R ) x. R ) mod P ) - ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) ) )
107 99 106 mpbid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P || ( ( ( ( -u 1 ^ R ) x. R ) mod P ) - ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) )
108 69 nnnn0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN0 )
109 7 9 zndvds 
 |-  ( ( P e. NN0 /\ ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ZZ /\ ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) e. ZZ ) -> ( ( L ` ( ( ( -u 1 ^ R ) x. R ) mod P ) ) = ( L ` ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) <-> P || ( ( ( ( -u 1 ^ R ) x. R ) mod P ) - ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) ) )
110 108 102 104 109 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( ( ( -u 1 ^ R ) x. R ) mod P ) ) = ( L ` ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) <-> P || ( ( ( ( -u 1 ^ R ) x. R ) mod P ) - ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) ) )
111 107 110 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( ( -u 1 ^ R ) x. R ) mod P ) ) = ( L ` ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) )
112 29 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L e. ( ZZring RingHom Y ) )
113 zringmulr 
 |-  x. = ( .r ` ZZring )
114 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
115 30 113 114 rhmmul 
 |-  ( ( L e. ( ZZring RingHom Y ) /\ ( ( -u 1 ^ R ) x. Q ) e. ZZ /\ ( 2 x. x ) e. ZZ ) -> ( L ` ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) = ( ( L ` ( ( -u 1 ^ R ) x. Q ) ) ( .r ` Y ) ( L ` ( 2 x. x ) ) ) )
116 112 103 65 115 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( ( -u 1 ^ R ) x. Q ) x. ( 2 x. x ) ) ) = ( ( L ` ( ( -u 1 ^ R ) x. Q ) ) ( .r ` Y ) ( L ` ( 2 x. x ) ) ) )
117 82 111 116 3eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) = ( ( L ` ( ( -u 1 ^ R ) x. Q ) ) ( .r ` Y ) ( L ` ( 2 x. x ) ) ) )
118 117 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( L ` ( ( -u 1 ^ R ) x. Q ) ) ( .r ` Y ) ( L ` ( 2 x. x ) ) ) ) )
119 32 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L : ZZ --> ( Base ` Y ) )
120 119 103 ffvelcdmd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ R ) x. Q ) ) e. ( Base ` Y ) )
121 119 65 ffvelcdmd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. x ) ) e. ( Base ` Y ) )
122 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 ) ) ) )
123 eqidd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) )
124 25 120 121 122 123 offval2 
 |-  ( ph -> ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( L ` ( ( -u 1 ^ R ) x. Q ) ) ( .r ` Y ) ( L ` ( 2 x. x ) ) ) ) )
125 118 124 eqtr4d 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) ) = ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) )
126 125 oveq2d 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) ) ) ) = ( G gsum ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) )
127 46 55 126 3eqtrd 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) = ( G gsum ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) )
128 8 114 mgpplusg 
 |-  ( .r ` Y ) = ( +g ` G )
129 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 ) ) )
130 eqid 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) )
131 15 128 24 25 120 121 129 130 gsummptfidmadd2 
 |-  ( ph -> ( G gsum ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) oF ( .r ` Y ) ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) )
132 127 131 eqtrd 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) = ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) )
133 132 oveq1d 
 |-  ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) )
134 eqid 
 |-  ( Unit ` Y ) = ( Unit ` Y )
135 134 8 unitsubm 
 |-  ( Y e. Ring -> ( Unit ` Y ) e. ( SubMnd ` G ) )
136 27 135 syl 
 |-  ( ph -> ( Unit ` Y ) e. ( SubMnd ` G ) )
137 elfzle2 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
138 137 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
139 62 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. RR )
140 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
141 uz2m1nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
142 67 140 141 3syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. NN )
143 142 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. RR )
144 2re 
 |-  2 e. RR
145 144 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. RR )
146 2pos 
 |-  0 < 2
147 146 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < 2 )
148 lemuldiv2 
 |-  ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
149 139 143 145 147 148 syl112anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
150 138 149 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) )
151 prmz 
 |-  ( P e. Prime -> P e. ZZ )
152 67 151 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ )
153 peano2zm 
 |-  ( P e. ZZ -> ( P - 1 ) e. ZZ )
154 152 153 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. ZZ )
155 fznn 
 |-  ( ( P - 1 ) e. ZZ -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
156 154 155 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
157 64 150 156 mpbir2and 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) )
158 fzm1ndvds 
 |-  ( ( P e. NN /\ ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( 2 x. x ) )
159 69 157 158 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( 2 x. x ) )
160 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
161 7 9 160 zndvds0 
 |-  ( ( P e. NN0 /\ ( 2 x. x ) e. ZZ ) -> ( ( L ` ( 2 x. x ) ) = ( 0g ` Y ) <-> P || ( 2 x. x ) ) )
162 108 65 161 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( 2 x. x ) ) = ( 0g ` Y ) <-> P || ( 2 x. x ) ) )
163 162 necon3abid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( 2 x. x ) ) =/= ( 0g ` Y ) <-> -. P || ( 2 x. x ) ) )
164 159 163 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. x ) ) =/= ( 0g ` Y ) )
165 20 simplbi 
 |-  ( Y e. Field -> Y e. DivRing )
166 19 165 syl 
 |-  ( ph -> Y e. DivRing )
167 166 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Y e. DivRing )
168 14 134 160 drngunit 
 |-  ( Y e. DivRing -> ( ( L ` ( 2 x. x ) ) e. ( Unit ` Y ) <-> ( ( L ` ( 2 x. x ) ) e. ( Base ` Y ) /\ ( L ` ( 2 x. x ) ) =/= ( 0g ` Y ) ) ) )
169 167 168 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( 2 x. x ) ) e. ( Unit ` Y ) <-> ( ( L ` ( 2 x. x ) ) e. ( Base ` Y ) /\ ( L ` ( 2 x. x ) ) =/= ( 0g ` Y ) ) ) )
170 121 164 169 mpbir2and 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. x ) ) e. ( Unit ` Y ) )
171 170 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( Unit ` Y ) )
172 fvexd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( 2 x. x ) ) e. _V )
173 130 25 172 42 fsuppmptdm 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) finSupp ( 0g ` G ) )
174 16 24 25 136 171 173 gsumsubmcl 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) e. ( Unit ` Y ) )
175 eqid 
 |-  ( /r ` Y ) = ( /r ` Y )
176 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
177 134 175 176 dvrid 
 |-  ( ( Y e. Ring /\ ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) e. ( Unit ` Y ) ) -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( 1r ` Y ) )
178 27 174 177 syl2anc 
 |-  ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( 1r ` Y ) )
179 120 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( Base ` Y ) )
180 fvexd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ R ) x. Q ) ) e. _V )
181 129 25 180 42 fsuppmptdm 
 |-  ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) finSupp ( 0g ` G ) )
182 15 16 24 25 179 181 gsumcl 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) e. ( Base ` Y ) )
183 14 134 175 114 dvrcan3 
 |-  ( ( Y e. Ring /\ ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) e. ( Base ` Y ) /\ ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) e. ( Unit ` Y ) ) -> ( ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) )
184 27 182 174 183 syl3anc 
 |-  ( ph -> ( ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) ( /r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( 2 x. x ) ) ) ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) )
185 133 178 184 3eqtr3rd 
 |-  ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) )