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 ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.2 ( 𝜑𝑄 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.3 ( 𝜑𝑃𝑄 )
lgseisen.4 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
lgseisen.5 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
lgseisen.6 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
lgseisen.7 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
lgseisen.8 𝐺 = ( mulGrp ‘ 𝑌 )
lgseisen.9 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion lgseisenlem3 ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) = ( 1r𝑌 ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 lgseisen.2 ( 𝜑𝑄 ∈ ( ℙ ∖ { 2 } ) )
3 lgseisen.3 ( 𝜑𝑃𝑄 )
4 lgseisen.4 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
5 lgseisen.5 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
6 lgseisen.6 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
7 lgseisen.7 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
8 lgseisen.8 𝐺 = ( mulGrp ‘ 𝑌 )
9 lgseisen.9 𝐿 = ( ℤRHom ‘ 𝑌 )
10 oveq2 ( 𝑘 = 𝑥 → ( 2 · 𝑘 ) = ( 2 · 𝑥 ) )
11 10 fveq2d ( 𝑘 = 𝑥 → ( 𝐿 ‘ ( 2 · 𝑘 ) ) = ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
12 11 cbvmptv ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
13 12 oveq2i ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
14 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
15 8 14 mgpbas ( Base ‘ 𝑌 ) = ( Base ‘ 𝐺 )
16 eqid ( 0g𝐺 ) = ( 0g𝐺 )
17 1 eldifad ( 𝜑𝑃 ∈ ℙ )
18 7 znfld ( 𝑃 ∈ ℙ → 𝑌 ∈ Field )
19 17 18 syl ( 𝜑𝑌 ∈ Field )
20 isfld ( 𝑌 ∈ Field ↔ ( 𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing ) )
21 20 simprbi ( 𝑌 ∈ Field → 𝑌 ∈ CRing )
22 19 21 syl ( 𝜑𝑌 ∈ CRing )
23 8 crngmgp ( 𝑌 ∈ CRing → 𝐺 ∈ CMnd )
24 22 23 syl ( 𝜑𝐺 ∈ CMnd )
25 fzfid ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin )
26 crngring ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
27 22 26 syl ( 𝜑𝑌 ∈ Ring )
28 9 zrhrhm ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
29 27 28 syl ( 𝜑𝐿 ∈ ( ℤring RingHom 𝑌 ) )
30 zringbas ℤ = ( Base ‘ ℤring )
31 30 14 rhmf ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
32 29 31 syl ( 𝜑𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
33 2z 2 ∈ ℤ
34 elfzelz ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑘 ∈ ℤ )
35 zmulcl ( ( 2 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 2 · 𝑘 ) ∈ ℤ )
36 33 34 35 sylancr ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 2 · 𝑘 ) ∈ ℤ )
37 ffvelrn ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) ∧ ( 2 · 𝑘 ) ∈ ℤ ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ ( Base ‘ 𝑌 ) )
38 32 36 37 syl2an ( ( 𝜑𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ ( Base ‘ 𝑌 ) )
39 38 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Base ‘ 𝑌 ) )
40 eqid ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) )
41 fvexd ( ( 𝜑𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ V )
42 fvexd ( 𝜑 → ( 0g𝐺 ) ∈ V )
43 40 25 41 42 fsuppmptdm ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) finSupp ( 0g𝐺 ) )
44 1 2 3 4 5 6 lgseisenlem2 ( 𝜑𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
45 15 16 24 25 39 43 44 gsumf1o ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) )
46 13 45 eqtr3id ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) )
47 1 2 3 4 5 lgseisenlem1 ( 𝜑𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
48 5 fmpt ( ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
49 47 48 sylibr ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
50 5 a1i ( 𝜑𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
51 eqidd ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) )
52 oveq2 ( 𝑘 = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) → ( 2 · 𝑘 ) = ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
53 52 fveq2d ( 𝑘 = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) = ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) )
54 49 50 51 53 fmptcof ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) )
55 54 oveq2d ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) ) )
56 2 eldifad ( 𝜑𝑄 ∈ ℙ )
57 56 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℙ )
58 prmz ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
59 57 58 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℤ )
60 2nn 2 ∈ ℕ
61 elfznn ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
62 61 adantl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℕ )
63 nnmulcl ( ( 2 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( 2 · 𝑥 ) ∈ ℕ )
64 60 62 63 sylancr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℕ )
65 64 nnzd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℤ )
66 59 65 zmulcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ )
67 17 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℙ )
68 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
69 67 68 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
70 66 69 zmodcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ∈ ℕ0 )
71 4 70 eqeltrid ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℕ0 )
72 71 nn0zd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℤ )
73 m1expcl ( 𝑅 ∈ ℤ → ( - 1 ↑ 𝑅 ) ∈ ℤ )
74 72 73 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℤ )
75 74 72 zmulcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ )
76 75 69 zmodcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ0 )
77 76 nn0cnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℂ )
78 2cnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℂ )
79 2ne0 2 ≠ 0
80 79 a1i ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ≠ 0 )
81 77 78 80 divcan2d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
82 81 fveq2d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) )
83 69 nnrpd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℝ+ )
84 eqidd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) )
85 4 oveq1i ( 𝑅 mod 𝑃 ) = ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 )
86 66 zred ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ )
87 modabs2 ( ( ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
88 86 83 87 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
89 85 88 syl5eq ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
90 74 74 72 66 83 84 89 modmul12d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) )
91 75 zred ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℝ )
92 modabs2 ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
93 91 83 92 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
94 74 zcnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℂ )
95 59 zcnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℂ )
96 65 zcnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℂ )
97 94 95 96 mulassd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) = ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) )
98 97 oveq1d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) )
99 90 93 98 3eqtr4d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) )
100 17 68 syl ( 𝜑𝑃 ∈ ℕ )
101 100 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
102 76 nn0zd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ )
103 74 59 zmulcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ∈ ℤ )
104 103 65 zmulcld ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ )
105 moddvds ( ( 𝑃 ∈ ℕ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
106 101 102 104 105 syl3anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
107 99 106 mpbid ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) )
108 69 nnnn0d ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ0 )
109 7 9 zndvds ( ( 𝑃 ∈ ℕ0 ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ ) → ( ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
110 108 102 104 109 syl3anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
111 107 110 mpbird ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) )
112 29 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
113 zringmulr · = ( .r ‘ ℤring )
114 eqid ( .r𝑌 ) = ( .r𝑌 )
115 30 113 114 rhmmul ( ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) ∧ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ∈ ℤ ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
116 112 103 65 115 syl3anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
117 82 111 116 3eqtrd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
118 117 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
119 32 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
120 119 103 ffvelrnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ∈ ( Base ‘ 𝑌 ) )
121 119 65 ffvelrnd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) )
122 eqidd ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) )
123 eqidd ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
124 25 120 121 122 123 offval2 ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
125 118 124 eqtr4d ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) = ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
126 125 oveq2d ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
127 46 55 126 3eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
128 8 114 mgpplusg ( .r𝑌 ) = ( +g𝐺 )
129 eqid ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) )
130 eqid ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
131 15 128 24 25 120 121 129 130 gsummptfidmadd2 ( 𝜑 → ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
132 127 131 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
133 132 oveq1d ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
134 eqid ( Unit ‘ 𝑌 ) = ( Unit ‘ 𝑌 )
135 134 8 unitsubm ( 𝑌 ∈ Ring → ( Unit ‘ 𝑌 ) ∈ ( SubMnd ‘ 𝐺 ) )
136 27 135 syl ( 𝜑 → ( Unit ‘ 𝑌 ) ∈ ( SubMnd ‘ 𝐺 ) )
137 elfzle2 ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
138 137 adantl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
139 62 nnred ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℝ )
140 prmuz2 ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ ‘ 2 ) )
141 uz2m1nn ( 𝑃 ∈ ( ℤ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
142 67 140 141 3syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ )
143 142 nnred ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
144 2re 2 ∈ ℝ
145 144 a1i ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℝ )
146 2pos 0 < 2
147 146 a1i ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 < 2 )
148 lemuldiv2 ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
149 139 143 145 147 148 syl112anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
150 138 149 mpbird ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) )
151 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
152 67 151 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℤ )
153 peano2zm ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
154 152 153 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℤ )
155 fznn ( ( 𝑃 − 1 ) ∈ ℤ → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
156 154 155 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
157 64 150 156 mpbir2and ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
158 fzm1ndvds ( ( 𝑃 ∈ ℕ ∧ ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
159 69 157 158 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
160 eqid ( 0g𝑌 ) = ( 0g𝑌 )
161 7 9 160 zndvds0 ( ( 𝑃 ∈ ℕ0 ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) = ( 0g𝑌 ) ↔ 𝑃 ∥ ( 2 · 𝑥 ) ) )
162 108 65 161 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) = ( 0g𝑌 ) ↔ 𝑃 ∥ ( 2 · 𝑥 ) ) )
163 162 necon3abid ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g𝑌 ) ↔ ¬ 𝑃 ∥ ( 2 · 𝑥 ) ) )
164 159 163 mpbird ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g𝑌 ) )
165 20 simplbi ( 𝑌 ∈ Field → 𝑌 ∈ DivRing )
166 19 165 syl ( 𝜑𝑌 ∈ DivRing )
167 166 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑌 ∈ DivRing )
168 14 134 160 drngunit ( 𝑌 ∈ DivRing → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) ↔ ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g𝑌 ) ) ) )
169 167 168 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) ↔ ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g𝑌 ) ) ) )
170 121 164 169 mpbir2and ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) )
171 170 fmpttd ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Unit ‘ 𝑌 ) )
172 fvexd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ V )
173 130 25 172 42 fsuppmptdm ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) finSupp ( 0g𝐺 ) )
174 16 24 25 136 171 173 gsumsubmcl ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) )
175 eqid ( /r𝑌 ) = ( /r𝑌 )
176 eqid ( 1r𝑌 ) = ( 1r𝑌 )
177 134 175 176 dvrid ( ( 𝑌 ∈ Ring ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) ) → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 1r𝑌 ) )
178 27 174 177 syl2anc ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 1r𝑌 ) )
179 120 fmpttd ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Base ‘ 𝑌 ) )
180 fvexd ( ( 𝜑𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ∈ V )
181 129 25 180 42 fsuppmptdm ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) finSupp ( 0g𝐺 ) )
182 15 16 24 25 179 181 gsumcl ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
183 14 134 175 114 dvrcan3 ( ( 𝑌 ∈ Ring ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) ) → ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) )
184 27 182 174 183 syl3anc ( 𝜑 → ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) )
185 133 178 184 3eqtr3rd ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) = ( 1r𝑌 ) )