Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥)) |
2 | 1 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥))) |
3 | 2 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
4 | 3 | oveq2i 6560 |
. . . . . 6
⊢ (𝐺 Σg
(𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
5 | | lgseisen.8 |
. . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝑌) |
6 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
7 | 5, 6 | mgpbas 18318 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝐺) |
8 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
9 | | lgseisen.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
10 | 9 | eldifad 3552 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
11 | | lgseisen.7 |
. . . . . . . . . . 11
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
12 | 11 | znfld 19728 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ Field) |
14 | | isfld 18579 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing)) |
15 | 14 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ CRing) |
17 | 5 | crngmgp 18378 |
. . . . . . . 8
⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CMnd) |
19 | | fzfid 12634 |
. . . . . . 7
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
20 | | crngring 18381 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Ring) |
22 | | lgseisen.9 |
. . . . . . . . . . . 12
⊢ 𝐿 = (ℤRHom‘𝑌) |
23 | 22 | zrhrhm 19679 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
25 | | zringbas 19643 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
26 | 25, 6 | rhmf 18549 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
27 | 24, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
28 | | 2z 11286 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
29 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ) |
30 | | zmulcl 11303 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝑘
∈ ℤ) → (2 · 𝑘) ∈ ℤ) |
31 | 28, 29, 30 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈
ℤ) |
32 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
33 | 27, 31, 32 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
34 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) |
35 | 33, 34 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
36 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐿‘(2 · 𝑘)) ∈ V |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V) |
38 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝐺) ∈ V |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
40 | 34, 19, 37, 39 | fsuppmptdm 8169 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) finSupp (0g‘𝐺)) |
41 | | lgseisen.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
42 | | lgseisen.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
43 | | lgseisen.4 |
. . . . . . . 8
⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) |
44 | | lgseisen.5 |
. . . . . . . 8
⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) |
45 | | lgseisen.6 |
. . . . . . . 8
⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) |
46 | 9, 41, 42, 43, 44, 45 | lgseisenlem2 24901 |
. . . . . . 7
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))) |
47 | 7, 8, 18, 19, 35, 40, 46 | gsumf1o 18140 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
48 | 4, 47 | syl5eqr 2658 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
49 | 9, 41, 42, 43, 44 | lgseisenlem1 24900 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) /
2))) |
50 | 44 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(1...((𝑃 − 1) /
2))((((-1↑𝑅) ·
𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) /
2))) |
51 | 49, 50 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2))) |
52 | 44 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) |
53 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) |
54 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) |
55 | 54 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) |
56 | 51, 52, 53, 55 | fmptcof 6304 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) |
57 | 56 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))) |
58 | 41 | eldifad 3552 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑄 ∈ ℙ) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ) |
60 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ) |
62 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℕ |
63 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
65 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℕ ∧ 𝑥
∈ ℕ) → (2 · 𝑥) ∈ ℕ) |
66 | 62, 64, 65 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℕ) |
67 | 66 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℤ) |
68 | 61, 67 | zmulcld 11364 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ) |
69 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
70 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
72 | 68, 71 | zmodcld 12553 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈
ℕ0) |
73 | 43, 72 | syl5eqel 2692 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈
ℕ0) |
74 | 73 | nn0zd 11356 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ) |
75 | | m1expcl 12745 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℤ →
(-1↑𝑅) ∈
ℤ) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℤ) |
77 | 76, 74 | zmulcld 11364 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ) |
78 | 77, 71 | zmodcld 12553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈
ℕ0) |
79 | 78 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ) |
80 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℂ) |
81 | | 2ne0 10990 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠
0) |
83 | 79, 80, 82 | divcan2d 10682 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((((-1↑𝑅) ·
𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃))) |
85 | 71 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℝ+) |
86 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃)) |
87 | 43 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) |
88 | 68 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ) |
89 | | modabs2 12566 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((𝑄 · (2
· 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
90 | 88, 85, 89 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
91 | 87, 90 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
92 | 76, 76, 74, 68, 85, 86, 91 | modmul12d 12586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
93 | 77 | zred 11358 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ) |
94 | | modabs2 12566 |
. . . . . . . . . . . . 13
⊢
((((-1↑𝑅)
· 𝑅) ∈ ℝ
∧ 𝑃 ∈
ℝ+) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
95 | 93, 85, 94 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
96 | 76 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℂ) |
97 | 61 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ) |
98 | 67 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℂ) |
99 | 96, 97, 98 | mulassd 9942 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) |
100 | 99 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
101 | 92, 95, 100 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃)) |
102 | 10, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℕ) |
103 | 102 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
104 | 78 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ) |
105 | 76, 61 | zmulcld 11364 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ) |
106 | 105, 67 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) |
107 | | moddvds 14829 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧
(((-1↑𝑅) ·
𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
108 | 103, 104,
106, 107 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
109 | 101, 108 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))) |
110 | 71 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℕ0) |
111 | 11, 22 | zndvds 19717 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ0
∧ (((-1↑𝑅)
· 𝑅) mod 𝑃) ∈ ℤ ∧
(((-1↑𝑅) ·
𝑄) · (2 ·
𝑥)) ∈ ℤ) →
((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
112 | 110, 104,
106, 111 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
113 | 109, 112 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥)))) |
114 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom
𝑌)) |
115 | | zringmulr 19646 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
116 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘𝑌) = (.r‘𝑌) |
117 | 25, 115, 116 | rhmmul 18550 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑌) ∧
((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2
· 𝑥) ∈ ℤ)
→ (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
118 | 114, 105,
67, 117 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
119 | 84, 113, 118 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
120 | 119 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
121 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
122 | 121, 105 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌)) |
123 | 121, 67 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌)) |
124 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) |
125 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
126 | 19, 122, 123, 124, 125 | offval2 6812 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
127 | 120, 126 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) |
128 | 127 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
129 | 48, 57, 128 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
130 | 5, 116 | mgpplusg 18316 |
. . . . 5
⊢
(.r‘𝑌) = (+g‘𝐺) |
131 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) |
132 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
133 | 7, 130, 18, 19, 122, 123, 131, 132 | gsummptfidmadd2 18149 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
134 | 129, 133 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
135 | 134 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((𝐺 Σ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 · 𝑥)))))) |
136 | | eqid 2610 |
. . . . . 6
⊢
(Unit‘𝑌) =
(Unit‘𝑌) |
137 | 136, 5 | unitsubm 18493 |
. . . . 5
⊢ (𝑌 ∈ Ring →
(Unit‘𝑌) ∈
(SubMnd‘𝐺)) |
138 | 21, 137 | syl 17 |
. . . 4
⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺)) |
139 | | elfzle2 12216 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
140 | 139 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
141 | 64 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ) |
142 | | prmuz2 15246 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
143 | | uz2m1nn 11639 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
144 | 69, 142, 143 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ) |
145 | 144 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ) |
146 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
147 | 146 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℝ) |
148 | | 2pos 10989 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
149 | 148 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 <
2) |
150 | | lemuldiv2 10783 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
151 | 141, 145,
147, 149, 150 | syl112anc 1322 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
152 | 140, 151 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1)) |
153 | | prmz 15227 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
154 | 69, 153 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
155 | | peano2zm 11297 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
156 | 154, 155 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ) |
157 | | fznn 12278 |
. . . . . . . . . 10
⊢ ((𝑃 − 1) ∈ ℤ
→ ((2 · 𝑥)
∈ (1...(𝑃 − 1))
↔ ((2 · 𝑥)
∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1)))) |
158 | 156, 157 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2
· 𝑥) ≤ (𝑃 − 1)))) |
159 | 66, 152, 158 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1))) |
160 | | fzm1ndvds 14882 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ (2
· 𝑥) ∈
(1...(𝑃 − 1))) →
¬ 𝑃 ∥ (2 ·
𝑥)) |
161 | 71, 159, 160 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥)) |
162 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑌) = (0g‘𝑌) |
163 | 11, 22, 162 | zndvds0 19718 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ0
∧ (2 · 𝑥) ∈
ℤ) → ((𝐿‘(2 · 𝑥)) = (0g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥))) |
164 | 110, 67, 163 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥))) |
165 | 164 | necon3abid 2818 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠
(0g‘𝑌)
↔ ¬ 𝑃 ∥ (2
· 𝑥))) |
166 | 161, 165 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)) |
167 | 14 | simplbi 475 |
. . . . . . . . 9
⊢ (𝑌 ∈ Field → 𝑌 ∈
DivRing) |
168 | 13, 167 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ DivRing) |
169 | 168 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing) |
170 | 6, 136, 162 | drngunit 18575 |
. . . . . . 7
⊢ (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)))) |
171 | 169, 170 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)))) |
172 | 123, 166,
171 | mpbir2and 959 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌)) |
173 | 172, 132 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌)) |
174 | | fvex 6113 |
. . . . . 6
⊢ (𝐿‘(2 · 𝑥)) ∈ V |
175 | 174 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V) |
176 | 132, 19, 175, 39 | fsuppmptdm 8169 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0g‘𝐺)) |
177 | 8, 18, 19, 138, 173, 176 | gsumsubmcl 18142 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) |
178 | | eqid 2610 |
. . . 4
⊢
(/r‘𝑌) = (/r‘𝑌) |
179 | | eqid 2610 |
. . . 4
⊢
(1r‘𝑌) = (1r‘𝑌) |
180 | 136, 178,
179 | dvrid 18511 |
. . 3
⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σg
(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
181 | 21, 177, 180 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
182 | 122, 131 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
183 | | fvex 6113 |
. . . . . 6
⊢ (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V |
184 | 183 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V) |
185 | 131, 19, 184, 39 | fsuppmptdm 8169 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0g‘𝐺)) |
186 | 7, 8, 18, 19, 182, 185 | gsumcl 18139 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌)) |
187 | 6, 136, 178, 116 | dvrcan3 18515 |
. . 3
⊢ ((𝑌 ∈ 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↑𝑅) · 𝑄))))) |
188 | 21, 186, 177, 187 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) |
189 | 135, 181,
188 | 3eqtr3rd 2653 |
1
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) |