MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgseisenlem4 Structured version   Visualization version   GIF version

Theorem lgseisenlem4 26535
Description: Lemma for lgseisen 26536. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)
Hypotheses
Ref Expression
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
Ref Expression
lgseisenlem4 (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))
Distinct variable groups:   𝑥,𝐺   𝑥,𝐿   𝑥,𝑦,𝑃   𝜑,𝑥,𝑦   𝑦,𝑀   𝑥,𝑄,𝑦   𝑥,𝑌   𝑥,𝑆
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝑆(𝑦)   𝐺(𝑦)   𝐿(𝑦)   𝑀(𝑥)   𝑌(𝑦)

Proof of Theorem lgseisenlem4
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 zringbas 20685 . . . . 5 ℤ = (Base‘ℤring)
2 zring0 20689 . . . . 5 0 = (0g‘ℤring)
3 zringabl 20683 . . . . . 6 ring ∈ Abel
4 ablcmn 19402 . . . . . 6 (ℤring ∈ Abel → ℤring ∈ CMnd)
53, 4mp1i 13 . . . . 5 (𝜑 → ℤring ∈ CMnd)
6 lgseisen.1 . . . . . . . . . 10 (𝜑𝑃 ∈ (ℙ ∖ {2}))
76eldifad 3900 . . . . . . . . 9 (𝜑𝑃 ∈ ℙ)
8 lgseisen.7 . . . . . . . . . 10 𝑌 = (ℤ/nℤ‘𝑃)
98znfld 20777 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑌 ∈ Field)
107, 9syl 17 . . . . . . . 8 (𝜑𝑌 ∈ Field)
11 isfld 20009 . . . . . . . . 9 (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
1211simprbi 497 . . . . . . . 8 (𝑌 ∈ Field → 𝑌 ∈ CRing)
1310, 12syl 17 . . . . . . 7 (𝜑𝑌 ∈ CRing)
14 lgseisen.8 . . . . . . . 8 𝐺 = (mulGrp‘𝑌)
1514crngmgp 19800 . . . . . . 7 (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
1613, 15syl 17 . . . . . 6 (𝜑𝐺 ∈ CMnd)
17 cmnmnd 19411 . . . . . 6 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
1816, 17syl 17 . . . . 5 (𝜑𝐺 ∈ Mnd)
19 fzfid 13702 . . . . 5 (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20 crngring 19804 . . . . . . . . . 10 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
2113, 20syl 17 . . . . . . . . 9 (𝜑𝑌 ∈ Ring)
22 lgseisen.9 . . . . . . . . . 10 𝐿 = (ℤRHom‘𝑌)
2322zrhrhm 20722 . . . . . . . . 9 (𝑌 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑌))
2421, 23syl 17 . . . . . . . 8 (𝜑𝐿 ∈ (ℤring RingHom 𝑌))
25 eqid 2739 . . . . . . . . 9 (Base‘𝑌) = (Base‘𝑌)
261, 25rhmf 19979 . . . . . . . 8 (𝐿 ∈ (ℤring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
2724, 26syl 17 . . . . . . 7 (𝜑𝐿:ℤ⟶(Base‘𝑌))
28 m1expcl 13814 . . . . . . . 8 (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℤ)
2928adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℤ)
3027, 29cofmpt 7013 . . . . . 6 (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))))
31 zringmpg 20702 . . . . . . . . 9 ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring)
3231, 14rhmmhm 19975 . . . . . . . 8 (𝐿 ∈ (ℤring RingHom 𝑌) → 𝐿 ∈ (((mulGrp‘ℂfld) ↾s ℤ) MndHom 𝐺))
3324, 32syl 17 . . . . . . 7 (𝜑𝐿 ∈ (((mulGrp‘ℂfld) ↾s ℤ) MndHom 𝐺))
34 neg1cn 12096 . . . . . . . . . . 11 -1 ∈ ℂ
35 neg1ne0 12098 . . . . . . . . . . 11 -1 ≠ 0
36 eqid 2739 . . . . . . . . . . . 12 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
37 eqid 2739 . . . . . . . . . . . 12 ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
3836, 37expghm 20706 . . . . . . . . . . 11 ((-1 ∈ ℂ ∧ -1 ≠ 0) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring GrpHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))))
3934, 35, 38mp2an 689 . . . . . . . . . 10 (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring GrpHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
40 ghmmhm 18853 . . . . . . . . . 10 ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring GrpHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))))
4139, 40ax-mp 5 . . . . . . . . 9 (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
42 cnring 20629 . . . . . . . . . 10 fld ∈ Ring
43 cnfldbas 20610 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
44 cnfld0 20631 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
45 cndrng 20636 . . . . . . . . . . . 12 fld ∈ DivRing
4643, 44, 45drngui 20006 . . . . . . . . . . 11 (ℂ ∖ {0}) = (Unit‘ℂfld)
4746, 36unitsubm 19921 . . . . . . . . . 10 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld)))
4842, 47ax-mp 5 . . . . . . . . 9 (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld))
4937resmhm2 18469 . . . . . . . . 9 (((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) ∧ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom (mulGrp‘ℂfld)))
5041, 48, 49mp2an 689 . . . . . . . 8 (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom (mulGrp‘ℂfld))
51 zsubrg 20660 . . . . . . . . . 10 ℤ ∈ (SubRing‘ℂfld)
5236subrgsubm 20046 . . . . . . . . . 10 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂfld)))
5351, 52ax-mp 5 . . . . . . . . 9 ℤ ∈ (SubMnd‘(mulGrp‘ℂfld))
5429fmpttd 6998 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ)
5554frnd 6617 . . . . . . . . 9 (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ)
56 eqid 2739 . . . . . . . . . 10 ((mulGrp‘ℂfld) ↾s ℤ) = ((mulGrp‘ℂfld) ↾s ℤ)
5756resmhm2b 18470 . . . . . . . . 9 ((ℤ ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ) → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom (mulGrp‘ℂfld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s ℤ))))
5853, 55, 57sylancr 587 . . . . . . . 8 (𝜑 → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom (mulGrp‘ℂfld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s ℤ))))
5950, 58mpbii 232 . . . . . . 7 (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s ℤ)))
60 mhmco 18471 . . . . . . 7 ((𝐿 ∈ (((mulGrp‘ℂfld) ↾s ℤ) MndHom 𝐺) ∧ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom ((mulGrp‘ℂfld) ↾s ℤ))) → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤring MndHom 𝐺))
6133, 59, 60syl2anc 584 . . . . . 6 (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤring MndHom 𝐺))
6230, 61eqeltrrd 2841 . . . . 5 (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤring MndHom 𝐺))
63 lgseisen.2 . . . . . . . . . . 11 (𝜑𝑄 ∈ (ℙ ∖ {2}))
6463gausslemma2dlem0a 26513 . . . . . . . . . 10 (𝜑𝑄 ∈ ℕ)
6564nnred 11997 . . . . . . . . 9 (𝜑𝑄 ∈ ℝ)
666gausslemma2dlem0a 26513 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ)
6765, 66nndivred 12036 . . . . . . . 8 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
6867adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ)
69 2nn 12055 . . . . . . . . 9 2 ∈ ℕ
70 elfznn 13294 . . . . . . . . . 10 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
7170adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
72 nnmulcl 12006 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
7369, 71, 72sylancr 587 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
7473nnred 11997 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℝ)
7568, 74remulcld 11014 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ)
7675flcld 13527 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
77 eqid 2739 . . . . . 6 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
78 fvexd 6798 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ V)
79 c0ex 10978 . . . . . . 7 0 ∈ V
8079a1i 11 . . . . . 6 (𝜑 → 0 ∈ V)
8177, 19, 78, 80fsuppmptdm 9148 . . . . 5 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) finSupp 0)
82 oveq2 7292 . . . . . 6 (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
8382fveq2d 6787 . . . . 5 (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
84 oveq2 7292 . . . . . 6 (𝑘 = (ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) = (-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
8584fveq2d 6787 . . . . 5 (𝑘 = (ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
861, 2, 5, 18, 19, 62, 76, 81, 83, 85gsummhm2 19549 . . . 4 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
8714, 25mgpbas 19735 . . . . . . 7 (Base‘𝑌) = (Base‘𝐺)
88 eqid 2739 . . . . . . . 8 (.r𝑌) = (.r𝑌)
8914, 88mgpplusg 19733 . . . . . . 7 (.r𝑌) = (+g𝐺)
9027adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
91 m1expcl 13814 . . . . . . . . 9 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
9276, 91syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
9390, 92ffvelrnd 6971 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌))
94 neg1z 12365 . . . . . . . . . 10 -1 ∈ ℤ
95 lgseisen.4 . . . . . . . . . . 11 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
9663eldifad 3900 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ ℙ)
9796adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
98 prmz 16389 . . . . . . . . . . . . . 14 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
9997, 98syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
10073nnzd 12434 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
10199, 100zmulcld 12441 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
1027adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
103 prmnn 16388 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
104102, 103syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
105101, 104zmodcld 13621 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ0)
10695, 105eqeltrid 2844 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
107 zexpcl 13806 . . . . . . . . . 10 ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ0) → (-1↑𝑅) ∈ ℤ)
10894, 106, 107sylancr 587 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
109108, 99zmulcld 12441 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
11090, 109ffvelrnd 6971 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
111 eqid 2739 . . . . . . 7 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
112 eqid 2739 . . . . . . 7 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
11387, 89, 16, 19, 93, 110, 111, 112gsummptfidmadd2 19536 . . . . . 6 (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
114 eqidd 2740 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
115 eqidd 2740 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
11619, 93, 110, 114, 115offval2 7562 . . . . . . . 8 (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))))
11724adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom 𝑌))
118 zringmulr 20688 . . . . . . . . . . . 12 · = (.r‘ℤring)
1191, 118, 88rhmmul 19980 . . . . . . . . . . 11 ((𝐿 ∈ (ℤring RingHom 𝑌) ∧ (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
120117, 92, 109, 119syl3anc 1370 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
121101zred 12435 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
122104nnrpd 12779 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
123 modval 13600 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
124121, 122, 123syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
12595, 124eqtrid 2791 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
12699zcnd 12436 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
12773nncnd 11998 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
128104nncnd 11998 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
129104nnne0d 12032 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ≠ 0)
130126, 127, 128, 129div23d 11797 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥)))
131130fveq2d 6787 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
132131oveq2d 7300 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
133132oveq2d 7300 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
134125, 133eqtrd 2779 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
135134oveq2d 7300 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
136 prmz 16389 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
137102, 136syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
138137, 76zmulcld 12441 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
139138zcnd 12436 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
140101zcnd 12436 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ)
141139, 140pncan3d 11344 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥)))
142 2cnd 12060 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
14371nncnd 11998 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ)
144126, 142, 143mul12d 11193 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥)))
145135, 141, 1443eqtrd 2783 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥)))
146145oveq2d 7300 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = (-1↑(2 · (𝑄 · 𝑥))))
14734a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
14835a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠ 0)
149106nn0zd 12433 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
150 expaddz 13836 . . . . . . . . . . . . . . . 16 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
151147, 148, 138, 149, 150syl22anc 836 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
152 expmulz 13838 . . . . . . . . . . . . . . . . . 18 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
153147, 148, 137, 76, 152syl22anc 836 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
154 1cnd 10979 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℂ)
155 eldifsni 4724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
1566, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ≠ 2)
157156necomd 3000 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 2 ≠ 𝑃)
158157neneqd 2949 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 2 = 𝑃)
159158adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃)
160 2z 12361 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℤ
161 uzid 12606 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
162160, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (ℤ‘2)
163 dvdsprm 16417 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
164162, 102, 163sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
165159, 164mtbird 325 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥ 𝑃)
166 oexpneg 16063 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃))
167154, 104, 165, 166syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃))
168 1exp 13821 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℤ → (1↑𝑃) = 1)
169137, 168syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1)
170169negeqd 11224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1)
171167, 170eqtrd 2779 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1)
172171oveq1d 7299 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
173153, 172eqtrd 2779 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
174173oveq1d 7299 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
175151, 174eqtrd 2779 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
176 nnmulcl 12006 . . . . . . . . . . . . . . . . . 18 ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ)
17764, 70, 176syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ)
178177nnnn0d 12302 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ0)
179 2nn0 12259 . . . . . . . . . . . . . . . . 17 2 ∈ ℕ0
180179a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ0)
181147, 178, 180expmuld 13876 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥)))
182 neg1sqe1 13922 . . . . . . . . . . . . . . . . 17 (-1↑2) = 1
183182oveq1i 7294 . . . . . . . . . . . . . . . 16 ((-1↑2)↑(𝑄 · 𝑥)) = (1↑(𝑄 · 𝑥))
184177nnzd 12434 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ)
185 1exp 13821 . . . . . . . . . . . . . . . . 17 ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1)
186184, 185syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1)
187183, 186eqtrid 2791 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑2)↑(𝑄 · 𝑥)) = 1)
188181, 187eqtrd 2779 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = 1)
189146, 175, 1883eqtr3d 2787 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1)
190189oveq1d 7299 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄))
19192zcnd 12436 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
192108zcnd 12436 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
193191, 192, 126mulassd 11007 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)))
194126mulid2d 11002 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄)
195190, 193, 1943eqtr3d 2787 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄)
196195fveq2d 6787 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿𝑄))
197120, 196eqtr3d 2781 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿𝑄))
198197mpteq2dva 5175 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄)))
199116, 198eqtrd 2779 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄)))
200199oveq2d 7300 . . . . . 6 (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄))))
201 lgseisen.3 . . . . . . . 8 (𝜑𝑃𝑄)
202 lgseisen.5 . . . . . . . 8 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
203 lgseisen.6 . . . . . . . 8 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
2046, 63, 201, 95, 202, 203, 8, 14, 22lgseisenlem3 26534 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r𝑌))
205204oveq2d 7300 . . . . . 6 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(1r𝑌)))
206113, 200, 2053eqtr3rd 2788 . . . . 5 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(1r𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄))))
207 eqid 2739 . . . . . . 7 (0g𝐺) = (0g𝐺)
20893fmpttd 6998 . . . . . . 7 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
209 fvexd 6798 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ V)
210 fvexd 6798 . . . . . . . 8 (𝜑 → (0g𝐺) ∈ V)
211111, 19, 209, 210fsuppmptdm 9148 . . . . . . 7 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) finSupp (0g𝐺))
21287, 207, 16, 19, 208, 211gsumcl 19525 . . . . . 6 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌))
213 eqid 2739 . . . . . . 7 (1r𝑌) = (1r𝑌)
21425, 88, 213ringridm 19820 . . . . . 6 ((𝑌 ∈ Ring ∧ (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(1r𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
21521, 212, 214syl2anc 584 . . . . 5 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r𝑌)(1r𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
21696, 98syl 17 . . . . . . . 8 (𝜑𝑄 ∈ ℤ)
21727, 216ffvelrnd 6971 . . . . . . 7 (𝜑 → (𝐿𝑄) ∈ (Base‘𝑌))
218 eqid 2739 . . . . . . . 8 (.g𝐺) = (.g𝐺)
21987, 218gsumconst 19544 . . . . . . 7 ((𝐺 ∈ Mnd ∧ (1...((𝑃 − 1) / 2)) ∈ Fin ∧ (𝐿𝑄) ∈ (Base‘𝑌)) → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄))) = ((♯‘(1...((𝑃 − 1) / 2)))(.g𝐺)(𝐿𝑄)))
22018, 19, 217, 219syl3anc 1370 . . . . . 6 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄))) = ((♯‘(1...((𝑃 − 1) / 2)))(.g𝐺)(𝐿𝑄)))
221 oddprm 16520 . . . . . . . . . 10 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
2226, 221syl 17 . . . . . . . . 9 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
223222nnnn0d 12302 . . . . . . . 8 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ0)
224 hashfz1 14069 . . . . . . . 8 (((𝑃 − 1) / 2) ∈ ℕ0 → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2))
225223, 224syl 17 . . . . . . 7 (𝜑 → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2))
226225oveq1d 7299 . . . . . 6 (𝜑 → ((♯‘(1...((𝑃 − 1) / 2)))(.g𝐺)(𝐿𝑄)) = (((𝑃 − 1) / 2)(.g𝐺)(𝐿𝑄)))
22731, 1mgpbas 19735 . . . . . . . . 9 ℤ = (Base‘((mulGrp‘ℂfld) ↾s ℤ))
228 eqid 2739 . . . . . . . . 9 (.g‘((mulGrp‘ℂfld) ↾s ℤ)) = (.g‘((mulGrp‘ℂfld) ↾s ℤ))
229227, 228, 218mhmmulg 18753 . . . . . . . 8 ((𝐿 ∈ (((mulGrp‘ℂfld) ↾s ℤ) MndHom 𝐺) ∧ ((𝑃 − 1) / 2) ∈ ℕ0𝑄 ∈ ℤ) → (𝐿‘(((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g𝐺)(𝐿𝑄)))
23033, 223, 216, 229syl3anc 1370 . . . . . . 7 (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g𝐺)(𝐿𝑄)))
23153a1i 11 . . . . . . . . . 10 (𝜑 → ℤ ∈ (SubMnd‘(mulGrp‘ℂfld)))
232 eqid 2739 . . . . . . . . . . 11 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
233232, 56, 228submmulg 18756 . . . . . . . . . 10 ((ℤ ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ((𝑃 − 1) / 2) ∈ ℕ0𝑄 ∈ ℤ) → (((𝑃 − 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄))
234231, 223, 216, 233syl3anc 1370 . . . . . . . . 9 (𝜑 → (((𝑃 − 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄))
235216zcnd 12436 . . . . . . . . . 10 (𝜑𝑄 ∈ ℂ)
236 cnfldexp 20640 . . . . . . . . . 10 ((𝑄 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ0) → (((𝑃 − 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
237235, 223, 236syl2anc 584 . . . . . . . . 9 (𝜑 → (((𝑃 − 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
238234, 237eqtr3d 2781 . . . . . . . 8 (𝜑 → (((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
239238fveq2d 6787 . . . . . . 7 (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(.g‘((mulGrp‘ℂfld) ↾s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
240230, 239eqtr3d 2781 . . . . . 6 (𝜑 → (((𝑃 − 1) / 2)(.g𝐺)(𝐿𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
241220, 226, 2403eqtrd 2783 . . . . 5 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
242206, 215, 2413eqtr3d 2787 . . . 4 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
243 subrgsubg 20039 . . . . . . . . . 10 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubGrp‘ℂfld))
24451, 243ax-mp 5 . . . . . . . . 9 ℤ ∈ (SubGrp‘ℂfld)
245 subgsubm 18786 . . . . . . . . 9 (ℤ ∈ (SubGrp‘ℂfld) → ℤ ∈ (SubMnd‘ℂfld))
246244, 245mp1i 13 . . . . . . . 8 (𝜑 → ℤ ∈ (SubMnd‘ℂfld))
24776fmpttd 6998 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) / 2))⟶ℤ)
248 df-zring 20680 . . . . . . . 8 ring = (ℂflds ℤ)
24919, 246, 247, 248gsumsubm 18482 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
25076zcnd 12436 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℂ)
25119, 250gsumfsum 20674 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
252249, 251eqtr3d 2781 . . . . . 6 (𝜑 → (ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
253252oveq2d 7300 . . . . 5 (𝜑 → (-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
254253fveq2d 6787 . . . 4 (𝜑 → (𝐿‘(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
25586, 242, 2543eqtr3d 2787 . . 3 (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
25666nnnn0d 12302 . . . 4 (𝜑𝑃 ∈ ℕ0)
257 zexpcl 13806 . . . . 5 ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ0) → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
258216, 223, 257syl2anc 584 . . . 4 (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
25919, 76fsumzcl 15456 . . . . 5 (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
260 m1expcl 13814 . . . . 5 𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
261259, 260syl 17 . . . 4 (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
2628, 22zndvds 20766 . . . 4 ((𝑃 ∈ ℕ0 ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
263256, 258, 261, 262syl3anc 1370 . . 3 (𝜑 → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
264255, 263mpbid 231 . 2 (𝜑𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
265 moddvds 15983 . . 3 ((𝑃 ∈ ℕ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
26666, 258, 261, 265syl3anc 1370 . 2 (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
267264, 266mpbird 256 1 (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2107  wne 2944  Vcvv 3433  cdif 3885  wss 3888  {csn 4562   class class class wbr 5075  cmpt 5158  ran crn 5591  ccom 5594  wf 6433  cfv 6437  (class class class)co 7284  f cof 7540  Fincfn 8742  cc 10878  cr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885  cmin 11214  -cneg 11215   / cdiv 11641  cn 11982  2c2 12037  0cn0 12242  cz 12328  cuz 12591  +crp 12739  ...cfz 13248  cfl 13519   mod cmo 13598  cexp 13791  chash 14053  Σcsu 15406  cdvds 15972  cprime 16385  Basecbs 16921  s cress 16950  .rcmulr 16972  0gc0g 17159   Σg cgsu 17160  Mndcmnd 18394   MndHom cmhm 18437  SubMndcsubmnd 18438  .gcmg 18709  SubGrpcsubg 18758   GrpHom cghm 18840  CMndccmn 19395  Abelcabl 19396  mulGrpcmgp 19729  1rcur 19746  Ringcrg 19792  CRingccrg 19793   RingHom crh 19965  DivRingcdr 20000  Fieldcfield 20001  SubRingcsubrg 20029  fldccnfld 20606  ringczring 20679  ℤRHomczrh 20710  ℤ/nczn 20713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-tpos 8051  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-oadd 8310  df-er 8507  df-ec 8509  df-qs 8513  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-xnn0 12315  df-z 12329  df-dec 12447  df-uz 12592  df-rp 12740  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-dvds 15973  df-gcd 16211  df-prm 16386  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-0g 17161  df-gsum 17162  df-imas 17228  df-qus 17229  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-mhm 18439  df-submnd 18440  df-grp 18589  df-minusg 18590  df-sbg 18591  df-mulg 18710  df-subg 18761  df-nsg 18762  df-eqg 18763  df-ghm 18841  df-cntz 18932  df-cmn 19397  df-abl 19398  df-mgp 19730  df-ur 19747  df-ring 19794  df-cring 19795  df-oppr 19871  df-dvdsr 19892  df-unit 19893  df-invr 19923  df-dvr 19934  df-rnghom 19968  df-drng 20002  df-field 20003  df-subrg 20031  df-lmod 20134  df-lss 20203  df-lsp 20243  df-sra 20443  df-rgmod 20444  df-lidl 20445  df-rsp 20446  df-2idl 20512  df-nzr 20538  df-rlreg 20563  df-domn 20564  df-idom 20565  df-cnfld 20607  df-zring 20680  df-zrh 20714  df-zn 20717
This theorem is referenced by:  lgseisen  26536
  Copyright terms: Public domain W3C validator