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 27436

Description: Lemma for lgseisen 27438. (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 7439	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
2	1	fveq2d 6911	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
3	2	cbvmptv 5261	. . . . . . 7 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
4	3	oveq2i 7442	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
6		eqid 2735	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
7	5, 6	mgpbas 20158	. . . . . . 7 ⊢ (Base‘𝑌) = (Base‘𝐺)
8		eqid 2735	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
9		lgseisen.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
10	9	eldifad 3975	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℙ)
11		lgseisen.7	. . . . . . . . . . 11 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
12	11	znfld 21597	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
13	10, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Field)
14		isfld 20757	. . . . . . . . . 10 ⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
15	14	simprbi 496	. . . . . . . . 9 ⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing)
16	13, 15	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ CRing)
17	5	crngmgp 20259	. . . . . . . 8 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
18	16, 17	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
19		fzfid 14011	. . . . . . 7 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20		crngring 20263	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
21	16, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
22		lgseisen.9	. . . . . . . . . . . 12 ⊢ 𝐿 = (ℤRHom‘𝑌)
23	22	zrhrhm 21540	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
24	21, 23	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25		zringbas 21482	. . . . . . . . . . 11 ⊢ ℤ = (Base‘ℤ_ring)
26	25, 6	rhmf 20502	. . . . . . . . . 10 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
27	24, 26	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
28		2z 12647	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
29		elfzelz 13561	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
30		zmulcl 12664	. . . . . . . . . 10 ⊢ ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
31	28, 29, 30	sylancr 587	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
32		ffvelcdm 7101	. . . . . . . . 9 ⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
33	27, 31, 32	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
34	33	fmpttd 7135	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
35		eqid 2735	. . . . . . . 8 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))
36		fvexd 6922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V)
37		fvexd 6922	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝐺) ∈ V)
38	35, 19, 36, 37	fsuppmptdm 9414	. . . . . . 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 27435	. . . . . . 7 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
45	7, 8, 18, 19, 34, 38, 44	gsumf1o 19949	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
46	4, 45	eqtr3id 2789	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
47	9, 39, 40, 41, 42	lgseisenlem1 27434	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
48	42	fmpt 7130	. . . . . . . 8 ⊢ (∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
49	47, 48	sylibr 234	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
50	42	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
51		eqidd 2736	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
52		oveq2 7439	. . . . . . . 8 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
53	52	fveq2d 6911	. . . . . . 7 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
54	49, 50, 51, 53	fmptcof 7150	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
55	54	oveq2d 7447	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
56	39	eldifad 3975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 ∈ ℙ)
57	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
58		prmz 16709	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
60		2nn 12337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℕ
61		elfznn 13590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
62	61	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
63		nnmulcl 12288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
64	60, 62, 63	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
65	64	nnzd 12638	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
66	59, 65	zmulcld 12726	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
67	10	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
68		prmnn 16708	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
70	66, 69	zmodcld 13929	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
71	41, 70	eqeltrid 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
72	71	nn0zd 12637	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
73		m1expcl 14124	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
74	72, 73	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
75	74, 72	zmulcld 12726	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
76	75, 69	zmodcld 13929	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
77	76	nn0cnd 12587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
78		2cnd 12342	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
79		2ne0 12368	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠ 0)
81	77, 78, 80	divcan2d 12043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
82	81	fveq2d 6911	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
83	69	nnrpd 13073	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ⁺)
84		eqidd 2736	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
85	41	oveq1i 7441	. . . . . . . . . . . . . 14 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
86	66	zred 12720	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
87		modabs2 13942	. . . . . . . . . . . . . . 15 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
88	86, 83, 87	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
89	85, 88	eqtrid 2787	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
90	74, 74, 72, 66, 83, 84, 89	modmul12d 13963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
91	75	zred 12720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ)
92		modabs2 13942	. . . . . . . . . . . . 13 ⊢ ((((-1↑𝑅) · 𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
93	91, 83, 92	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
94	74	zcnd 12721	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
95	59	zcnd 12721	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
96	65	zcnd 12721	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
97	94, 95, 96	mulassd 11282	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
98	97	oveq1d 7446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
99	90, 93, 98	3eqtr4d 2785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃))
100	10, 68	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
101	100	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
102	76	nn0zd 12637	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
103	74, 59	zmulcld 12726	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
104	103, 65	zmulcld 12726	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
105		moddvds 16298	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
106	101, 102, 104, 105	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
107	99, 106	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
108	69	nnnn0d 12585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ₀)
109	11, 22	zndvds 21586	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ₀ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
110	108, 102, 104, 109	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
111	107, 110	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
112	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
113		zringmulr 21486	. . . . . . . . . . 11 ⊢ · = (._r‘ℤ_ring)
114		eqid 2735	. . . . . . . . . . 11 ⊢ (._r‘𝑌) = (._r‘𝑌)
115	25, 113, 114	rhmmul 20503	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
116	112, 103, 65, 115	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
117	82, 111, 116	3eqtrd 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
118	117	mpteq2dva 5248	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
119	27	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
120	119, 103	ffvelcdmd 7105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
121	119, 65	ffvelcdmd 7105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
122		eqidd 2736	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
123		eqidd 2736	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
124	19, 120, 121, 122, 123	offval2 7717	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
125	118, 124	eqtr4d 2778	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
126	125	oveq2d 7447	. . . . 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 2779	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
128	5, 114	mgpplusg 20156	. . . . 5 ⊢ (._r‘𝑌) = (+_g‘𝐺)
129		eqid 2735	. . . . 5 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
130		eqid 2735	. . . . 5 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
131	7, 128, 18, 19, 120, 121, 129, 130	gsummptfidmadd2 19959	. . . 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 2775	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
133	132	oveq1d 7446	. 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 2735	. . . . . 6 ⊢ (Unit‘𝑌) = (Unit‘𝑌)
135	134, 5	unitsubm 20403	. . . . 5 ⊢ (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
136	21, 135	syl 17	. . . 4 ⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
137		elfzle2 13565	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
138	137	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
139	62	nnred 12279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
140		prmuz2 16730	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
141		uz2m1nn 12963	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
142	67, 140, 141	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
143	142	nnred 12279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
144		2re 12338	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
145	144	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
146		2pos 12367	. . . . . . . . . . . 12 ⊢ 0 < 2
147	146	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
148		lemuldiv2 12147	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
149	139, 143, 145, 147, 148	syl112anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
150	138, 149	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
151		prmz 16709	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
152	67, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153		peano2zm 12658	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
154	152, 153	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ)
155		fznn 13629	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
156	154, 155	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
157	64, 150, 156	mpbir2and 713	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
158		fzm1ndvds 16356	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
159	69, 157, 158	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
160		eqid 2735	. . . . . . . . . 10 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
161	11, 22, 160	zndvds0 21587	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ₀ ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) = (0_g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
162	108, 65, 161	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0_g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
163	162	necon3abid 2975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌) ↔ ¬ 𝑃 ∥ (2 · 𝑥)))
164	159, 163	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))
165	14	simplbi 497	. . . . . . . . 9 ⊢ (𝑌 ∈ Field → 𝑌 ∈ DivRing)
166	13, 165	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ DivRing)
167	166	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing)
168	6, 134, 160	drngunit 20751	. . . . . . 7 ⊢ (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))))
169	167, 168	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0_g‘𝑌))))
170	121, 164, 169	mpbir2and 713	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌))
171	170	fmpttd 7135	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
172		fvexd 6922	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V)
173	130, 19, 172, 37	fsuppmptdm 9414	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0_g‘𝐺))
174	8, 18, 19, 136, 171, 173	gsumsubmcl 19952	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
175		eqid 2735	. . . 4 ⊢ (/_r‘𝑌) = (/_r‘𝑌)
176		eqid 2735	. . . 4 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
177	134, 175, 176	dvrid 20423	. . 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 584	. 2 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1_r‘𝑌))
179	120	fmpttd 7135	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
180		fvexd 6922	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V)
181	129, 19, 180, 37	fsuppmptdm 9414	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0_g‘𝐺))
182	7, 8, 18, 19, 179, 181	gsumcl 19948	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
183	6, 134, 175, 114	dvrcan3 20427	. . 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 1370	. 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 2784	1 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 Vcvv 3478 ∖ cdif 3960 {csn 4631 class class class wbr 5148 ↦ cmpt 5231 ∘ ccom 5693 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ∘_f cof 7695 Fincfn 8984 ℝcr 11152 0cc0 11153 1c1 11154 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 -cneg 11491 / cdiv 11918 ℕcn 12264 2c2 12319 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 ℝ⁺crp 13032 ...cfz 13544 mod cmo 13906 ↑cexp 14099 ∥ cdvds 16287 ℙcprime 16705 Basecbs 17245 ._rcmulr 17299 0_gc0g 17486 Σ_g cgsu 17487 SubMndcsubmnd 18808 CMndccmn 19813 mulGrpcmgp 20152 1_rcur 20199 Ringcrg 20251 CRingccrg 20252 Unitcui 20372 /_rcdvr 20417 RingHom crh 20486 DivRingcdr 20746 Fieldcfield 20747 ℤ_ringczring 21475 ℤRHomczrh 21528 ℤ/nℤczn 21531

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232 ax-mulf 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-tpos 8250 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-er 8744 df-ec 8746 df-qs 8750 df-map 8867 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-sup 9480 df-inf 9481 df-oi 9548 df-dju 9939 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-xnn0 12598 df-z 12612 df-dec 12732 df-uz 12877 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-dvds 16288 df-gcd 16529 df-prm 16706 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-0g 17488 df-gsum 17489 df-imas 17555 df-qus 17556 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-mhm 18809 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-nsg 19155 df-eqg 19156 df-ghm 19244 df-cntz 19348 df-cmn 19815 df-abl 19816 df-mgp 20153 df-rng 20171 df-ur 20200 df-ring 20253 df-cring 20254 df-oppr 20351 df-dvdsr 20374 df-unit 20375 df-invr 20405 df-dvr 20418 df-rhm 20489 df-nzr 20530 df-subrng 20563 df-subrg 20587 df-rlreg 20711 df-domn 20712 df-idom 20713 df-drng 20748 df-field 20749 df-lmod 20877 df-lss 20948 df-lsp 20988 df-sra 21190 df-rgmod 21191 df-lidl 21236 df-rsp 21237 df-2idl 21278 df-cnfld 21383 df-zring 21476 df-zrh 21532 df-zn 21535

This theorem is referenced by: lgseisenlem4 27437

W3C validator