lgseisenlem3 - Metamath Proof Explorer

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

Theorem lgseisenlem3 27517

Description: Lemma for lgseisen 27519. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-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
lgseisenlem3	⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))

Distinct variable groups: 𝑥,𝐺 𝑥,𝐿 𝑥,𝑦,𝑃 𝜑,𝑥,𝑦 𝑦,𝑀 𝑥,𝑄,𝑦 𝑥,𝑌 𝑥,𝑆 Allowed substitution hints: 𝑅(𝑥,𝑦) 𝑆(𝑦) 𝐺(𝑦) 𝐿(𝑦) 𝑀(𝑥) 𝑌(𝑦)

Proof of Theorem lgseisenlem3 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7418	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
2	1	fveq2d 6885	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
3	2	cbvmptv 5214	. . . . . . 7 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
4	3	oveq2i 7421	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
6		eqid 2761	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
7	5, 6	mgpbas 20220	. . . . . . 7 ⊢ (Base‘𝑌) = (Base‘𝐺)
8		eqid 2761	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
9		lgseisen.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
10	9	eldifad 3916	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℙ)
11		lgseisen.7	. . . . . . . . . . 11 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
12	11	znfld 21689	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
13	10, 12	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Field)
14		isfld 20825	. . . . . . . . . 10 ⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
15	14	simprbi 502	. . . . . . . . 9 ⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing)
16	13, 15	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ CRing)
17	5	crngmgp 20322	. . . . . . . 8 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
18	16, 17	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
19		fzfid 14008	. . . . . . 7 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20		crngring 20326	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
21	16, 20	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
22		lgseisen.9	. . . . . . . . . . . 12 ⊢ 𝐿 = (ℤRHom‘𝑌)
23	22	zrhrhm 21640	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
24	21, 23	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25		zringbas 21582	. . . . . . . . . . 11 ⊢ ℤ = (Base‘ℤ_ring)
26	25, 6	rhmf 20565	. . . . . . . . . 10 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
27	24, 26	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
28		2z 12625	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
29		elfzelz 13551	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
30		zmulcl 12642	. . . . . . . . . 10 ⊢ ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
31	28, 29, 30	sylancr 598	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
32		ffvelcdm 7076	. . . . . . . . 9 ⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
33	27, 31, 32	syl2an 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
34	33	fmpttd 7110	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
35		eqid 2761	. . . . . . . 8 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))
36		fvexd 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V)
37		fvexd 6896	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝐺) ∈ V)
38	35, 19, 36, 37	fsuppmptdm 9335	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) finSupp (0_g‘𝐺))
39		lgseisen.2	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
40		lgseisen.3	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
41		lgseisen.4	. . . . . . . 8 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
42		lgseisen.5	. . . . . . . 8 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
43		lgseisen.6	. . . . . . . 8 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
44	9, 39, 40, 41, 42, 43	lgseisenlem2 27516	. . . . . . 7 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
45	7, 8, 18, 19, 34, 38, 44	gsumf1o 19985	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
46	4, 45	eqtr3id 2810	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
47	9, 39, 40, 41, 42	lgseisenlem1 27515	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
48	42	fmpt 7105	. . . . . . . 8 ⊢ (∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
49	47, 48	sylibr 237	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
50	42	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
51		eqidd 2762	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
52		oveq2 7418	. . . . . . . 8 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
53	52	fveq2d 6885	. . . . . . 7 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
54	49, 50, 51, 53	fmptcof 7126	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
55	54	oveq2d 7426	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
56	39	eldifad 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 ∈ ℙ)
57	56	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
58		prmz 16732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
59	57, 58	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
60		2nn 12313	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℕ
61		elfznn 13580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
62	61	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
63		nnmulcl 12256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
64	60, 62, 63	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
65	64	nnzd 12616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
66	59, 65	zmulcld 12705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
67	10	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
68		prmnn 16731	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
69	67, 68	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
70	66, 69	zmodcld 13924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
71	41, 70	eqeltrid 2865	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
72	71	nn0zd 12615	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
73		m1expcl 14121	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
74	72, 73	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
75	74, 72	zmulcld 12705	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
76	75, 69	zmodcld 13924	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
77	76	nn0cnd 12566	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
78		2cnd 12318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
79		2ne0 12346	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠ 0)
81	77, 78, 80	divcan2d 11992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
82	81	fveq2d 6885	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
83	69	nnrpd 13057	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ⁺)
84		eqidd 2762	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
85	41	oveq1i 7420	. . . . . . . . . . . . . 14 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
86	66	zred 12699	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
87		modabs2 13937	. . . . . . . . . . . . . . 15 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
88	86, 83, 87	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
89	85, 88	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
90	74, 74, 72, 66, 83, 84, 89	modmul12d 13960	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
91	75	zred 12699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ)
92		modabs2 13937	. . . . . . . . . . . . 13 ⊢ ((((-1↑𝑅) · 𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
93	91, 83, 92	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
94	74	zcnd 12700	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
95	59	zcnd 12700	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
96	65	zcnd 12700	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
97	94, 95, 96	mulassd 11231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
98	97	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
99	90, 93, 98	3eqtr4d 2806	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃))
100	10, 68	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
101	100	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
102	76	nn0zd 12615	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
103	74, 59	zmulcld 12705	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
104	103, 65	zmulcld 12705	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
105		moddvds 16320	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
106	101, 102, 104, 105	syl3anc 1396	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
107	99, 106	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
108	69	nnnn0d 12564	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ₀)
109	11, 22	zndvds 21678	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ₀ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
110	108, 102, 104, 109	syl3anc 1396	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
111	107, 110	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
112	24	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
113		zringmulr 21586	. . . . . . . . . . 11 ⊢ · = (._r‘ℤ_ring)
114		eqid 2761	. . . . . . . . . . 11 ⊢ (._r‘𝑌) = (._r‘𝑌)
115	25, 113, 114	rhmmul 20567	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
116	112, 103, 65, 115	syl3anc 1396	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
117	82, 111, 116	3eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
118	117	mpteq2dva 5203	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
119	27	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
120	119, 103	ffvelcdmd 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
121	119, 65	ffvelcdmd 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
122		eqidd 2762	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
123		eqidd 2762	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
124	19, 120, 121, 122, 123	offval2 7694	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
125	118, 124	eqtr4d 2799	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
126	125	oveq2d 7426	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
127	46, 55, 126	3eqtrd 2800	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
128	5, 114	mgpplusg 20219	. . . . 5 ⊢ (._r‘𝑌) = (+_g‘𝐺)
129		eqid 2761	. . . . 5 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
130		eqid 2761	. . . . 5 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
131	7, 128, 18, 19, 120, 121, 129, 130	gsummptfidmadd2 19995	. . . 4 ⊢ (𝜑 → (𝐺 Σ_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 2796	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
133	132	oveq1d 7425	. 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 · 𝑥))))))
134		eqid 2761	. . . . . 6 ⊢ (Unit‘𝑌) = (Unit‘𝑌)
135	134, 5	unitsubm 20467	. . . . 5 ⊢ (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
136	21, 135	syl 18	. . . 4 ⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
137		elfzle2 13555	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
138	137	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
139	62	nnred 12247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
140		prmuz2 16753	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
141		uz2m1nn 12946	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
142	67, 140, 141	3syl 19	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
143	142	nnred 12247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
144		2re 12314	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
145	144	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
146		2pos 12344	. . . . . . . . . . . 12 ⊢ 0 < 2
147	146	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
148		lemuldiv2 12095	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
149	139, 143, 145, 147, 148	syl112anc 1399	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
150	138, 149	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
151		prmz 16732	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
152	67, 151	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153		peano2zm 12636	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
154	152, 153	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ)
155		fznn 13619	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
156	154, 155	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
157	64, 150, 156	mpbir2and 725	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
158		fzm1ndvds 16379	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
159	69, 157, 158	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
160		eqid 2761	. . . . . . . . . 10 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
161	11, 22, 160	zndvds0 21679	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ₀ ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) = (0_g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
162	108, 65, 161	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0_g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
163	162	necon3abid 2992	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌) ↔ ¬ 𝑃 ∥ (2 · 𝑥)))
164	159, 163	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))
165	14	simplbi 501	. . . . . . . . 9 ⊢ (𝑌 ∈ Field → 𝑌 ∈ DivRing)
166	13, 165	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ DivRing)
167	166	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing)
168	6, 134, 160	drngunit 20817	. . . . . . 7 ⊢ (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))))
169	167, 168	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))))
170	121, 164, 169	mpbir2and 725	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌))
171	170	fmpttd 7110	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
172		fvexd 6896	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V)
173	130, 19, 172, 37	fsuppmptdm 9335	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0_g‘𝐺))
174	8, 18, 19, 136, 171, 173	gsumsubmcl 19988	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
175		eqid 2761	. . . 4 ⊢ (/_r‘𝑌) = (/_r‘𝑌)
176		eqid 2761	. . . 4 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
177	134, 175, 176	dvrid 20487	. . 3 ⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1_r‘𝑌))
178	21, 174, 177	syl2anc 595	. 2 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1_r‘𝑌))
179	120	fmpttd 7110	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
180		fvexd 6896	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V)
181	129, 19, 180, 37	fsuppmptdm 9335	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0_g‘𝐺))
182	7, 8, 18, 19, 179, 181	gsumcl 19984	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
183	6, 134, 175, 114	dvrcan3 20491	. . 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↑𝑅) · 𝑄)))))
184	21, 182, 174, 183	syl3anc 1396	. 2 ⊢ (𝜑 → (((𝐺 Σ_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 2805	1 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 Vcvv 3453 ∖ cdif 3901 {csn 4588 class class class wbr 5108 ↦ cmpt 5191 ∘ ccom 5665 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∘_f cof 7672 Fincfn 8942 ℝcr 11098 0cc0 11099 1c1 11100 · cmul 11104 < clt 11242 ≤ cle 11243 − cmin 11440 -cneg 11441 / cdiv 11870 ℕcn 12232 2c2 12294 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ℝ⁺crp 13015 ...cfz 13534 mod cmo 13901 ↑cexp 14096 ∥ cdvds 16309 ℙcprime 16728 Basecbs 17268 ._rcmulr 17310 0_gc0g 17491 Σ_g cgsu 17492 SubMndcsubmnd 18839 CMndccmn 19849 mulGrpcmgp 20215 1_rcur 20262 Ringcrg 20314 CRingccrg 20315 Unitcui 20436 /_rcdvr 20481 RingHom crh 20550 DivRingcdr 20812 Fieldcfield 20813 ℤ_ringczring 21575 ℤRHomczrh 21628 ℤ/nℤczn 21631

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177 ax-addf 11178 ax-mulf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-ec 8695 df-qs 8699 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-inf 9402 df-oi 9471 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-fl 13824 df-mod 13902 df-seq 14037 df-exp 14097 df-hash 14366 df-cj 15149 df-re 15150 df-im 15151 df-sqrt 15285 df-abs 15286 df-dvds 16310 df-gcd 16552 df-prm 16729 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-0g 17493 df-gsum 17494 df-imas 17561 df-qus 17562 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-nsg 19189 df-eqg 19190 df-ghm 19283 df-cntz 19386 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-rhm 20553 df-nzr 20595 df-subrng 20630 df-subrg 20654 df-rlreg 20778 df-domn 20779 df-idom 20780 df-drng 20814 df-field 20815 df-lmod 20962 df-lss 21032 df-lsp 21072 df-sra 21273 df-rgmod 21274 df-lidl 21311 df-rsp 21312 df-2idl 21368 df-cnfld 21502 df-zring 21576 df-zrh 21632 df-zn 21635

This theorem is referenced by: lgseisenlem4 27518

W3C validator