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 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ∈ ( Base ‘ 𝑌 ) )
121 119 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ‘ 𝑌 ) )