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 ffvelrn
 |-  ( ( 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 syl5eq
 |-  ( ( 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 ffvelrnd
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ R ) x. Q ) ) e. ( Base ` Y ) )
121 119 65 ffvelrnd
 |-  ( ( 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 ) )