Theorem lgseisenlem3

Description: Lemma for lgseisen . (Contributed by Mario Carneiro, 17-Jun-2015) (Proof shortened by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lgseisen.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	lgseisen.2	⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
	lgseisen.3	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
	lgseisen.4	⊢ 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
	lgseisen.5	⊢ 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
	lgseisen.6	⊢ 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
	lgseisen.7	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
	lgseisen.8	⊢ 𝐺 = ( mulGrp ‘ 𝑌 )
	lgseisen.9	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion	lgseisenlem3	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) = ( 1r ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		lgseisen.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		lgseisen.2	⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
3		lgseisen.3	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
4		lgseisen.4	⊢ 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
5		lgseisen.5	⊢ 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
6		lgseisen.6	⊢ 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
7		lgseisen.7	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
8		lgseisen.8	⊢ 𝐺 = ( mulGrp ‘ 𝑌 )
9		lgseisen.9	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
10		oveq2	⊢ ( 𝑘 = 𝑥 → ( 2 · 𝑘 ) = ( 2 · 𝑥 ) )
11	10	fveq2d	⊢ ( 𝑘 = 𝑥 → ( 𝐿 ‘ ( 2 · 𝑘 ) ) = ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
12	11	cbvmptv	⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
13	12	oveq2i	⊢ ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
14		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
15	8 14	mgpbas	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝐺 )
16		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
17	1	eldifad	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
18	7	znfld	⊢ ( 𝑃 ∈ ℙ → 𝑌 ∈ Field )
19	17 18	syl	⊢ ( 𝜑 → 𝑌 ∈ Field )
20		isfld	⊢ ( 𝑌 ∈ Field ↔ ( 𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing ) )
21	20	simprbi	⊢ ( 𝑌 ∈ Field → 𝑌 ∈ CRing )
22	19 21	syl	⊢ ( 𝜑 → 𝑌 ∈ CRing )
23	8	crngmgp	⊢ ( 𝑌 ∈ CRing → 𝐺 ∈ CMnd )
24	22 23	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
25		fzfid	⊢ ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin )
26		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
27	22 26	syl	⊢ ( 𝜑 → 𝑌 ∈ Ring )
28	9	zrhrhm	⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
29	27 28	syl	⊢ ( 𝜑 → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
30		zringbas	⊢ ℤ = ( Base ‘ ℤring )
31	30 14	rhmf	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
32	29 31	syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
33		2z	⊢ 2 ∈ ℤ
34		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑘 ∈ ℤ )
35		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 2 · 𝑘 ) ∈ ℤ )
36	33 34 35	sylancr	⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 2 · 𝑘 ) ∈ ℤ )
37		ffvelcdm	⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) ∧ ( 2 · 𝑘 ) ∈ ℤ ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ ( Base ‘ 𝑌 ) )
38	32 36 37	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ ( Base ‘ 𝑌 ) )
39	38	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Base ‘ 𝑌 ) )
40		eqid	⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) )
41		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) ∈ V )
42		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
43	40 25 41 42	fsuppmptdm	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) finSupp ( 0g ‘ 𝐺 ) )
44	1 2 3 4 5 6	lgseisenlem2	⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
45	15 16 24 25 39 43 44	gsumf1o	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) )
46	13 45	eqtr3id	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) )
47	1 2 3 4 5	lgseisenlem1	⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
48	5	fmpt	⊢ ( ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
49	47 48	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
50	5	a1i	⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
51		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) = ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) )
52		oveq2	⊢ ( 𝑘 = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) → ( 2 · 𝑘 ) = ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
53	52	fveq2d	⊢ ( 𝑘 = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) → ( 𝐿 ‘ ( 2 · 𝑘 ) ) = ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) )
54	49 50 51 53	fmptcof	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) )
55	54	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑘 ) ) ) ∘ 𝑀 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) ) )
56	2	eldifad	⊢ ( 𝜑 → 𝑄 ∈ ℙ )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℙ )
58		prmz	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
59	57 58	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℤ )
60		2nn	⊢ 2 ∈ ℕ
61		elfznn	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
62	61	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℕ )
63		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( 2 · 𝑥 ) ∈ ℕ )
64	60 62 63	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℕ )
65	64	nnzd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℤ )
66	59 65	zmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ )
67	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℙ )
68		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
69	67 68	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
70	66 69	zmodcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ∈ ℕ0 )
71	4 70	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℕ0 )
72	71	nn0zd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℤ )
73		m1expcl	⊢ ( 𝑅 ∈ ℤ → ( - 1 ↑ 𝑅 ) ∈ ℤ )
74	72 73	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℤ )
75	74 72	zmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ )
76	75 69	zmodcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ0 )
77	76	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℂ )
78		2cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℂ )
79		2ne0	⊢ 2 ≠ 0
80	79	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ≠ 0 )
81	77 78 80	divcan2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
82	81	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) )
83	69	nnrpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℝ+ )
84		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) )
85	4	oveq1i	⊢ ( 𝑅 mod 𝑃 ) = ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 )
86	66	zred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ )
87		modabs2	⊢ ( ( ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
88	86 83 87	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
89	85 88	eqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
90	74 74 72 66 83 84 89	modmul12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) )
91	75	zred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℝ )
92		modabs2	⊢ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
93	91 83 92	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
94	74	zcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℂ )
95	59	zcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℂ )
96	65	zcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℂ )
97	94 95 96	mulassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) = ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) )
98	97	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) )
99	90 93 98	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) )
100	17 68	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
102	76	nn0zd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ )
103	74 59	zmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ∈ ℤ )
104	103 65	zmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ )
105		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
106	101 102 104 105	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
107	99 106	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) )
108	69	nnnn0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ0 )
109	7 9	zndvds	⊢ ( ( 𝑃 ∈ ℕ0 ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ∈ ℤ ) → ( ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
110	108 102 104 109	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ↔ 𝑃 ∥ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) − ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) ) )
111	107 110	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) = ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) )
112	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
113		zringmulr	⊢ · = ( .r ‘ ℤring )
114		eqid	⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
115	30 113 114	rhmmul	⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) ∧ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ∈ ℤ ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
116	112 103 65 115	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( ( - 1 ↑ 𝑅 ) · 𝑄 ) · ( 2 · 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
117	82 111 116	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) = ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
118	117	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
119	32	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
120	119 103	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ∈ ( Base ‘ 𝑌 ) )
121	119 65	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) )
122		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) )
123		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) )
124	25 120 121 122 123	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r ‘ 𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
125	118 124	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) = ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r ‘ 𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) )
126	125	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) ) ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r ‘ 𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
127	46 55 126	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r ‘ 𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
128	8 114	mgpplusg	⊢ ( .r ‘ 𝑌 ) = ( +g ‘ 𝐺 )
129		eqid	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) )
130		eqid	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) )
131	15 128 24 25 120 121 129 130	gsummptfidmadd2	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ∘f ( .r ‘ 𝑌 ) ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
132	127 131	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
133	132	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) )
134		eqid	⊢ ( Unit ‘ 𝑌 ) = ( Unit ‘ 𝑌 )
135	134 8	unitsubm	⊢ ( 𝑌 ∈ Ring → ( Unit ‘ 𝑌 ) ∈ ( SubMnd ‘ 𝐺 ) )
136	27 135	syl	⊢ ( 𝜑 → ( Unit ‘ 𝑌 ) ∈ ( SubMnd ‘ 𝐺 ) )
137		elfzle2	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
138	137	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
139	62	nnred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℝ )
140		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
141		uz2m1nn	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
142	67 140 141	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ )
143	142	nnred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
144		2re	⊢ 2 ∈ ℝ
145	144	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℝ )
146		2pos	⊢ 0 < 2
147	146	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 < 2 )
148		lemuldiv2	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
149	139 143 145 147 148	syl112anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
150	138 149	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) )
151		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
152	67 151	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℤ )
153		peano2zm	⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
154	152 153	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℤ )
155		fznn	⊢ ( ( 𝑃 − 1 ) ∈ ℤ → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
156	154 155	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
157	64 150 156	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
158		fzm1ndvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
159	69 157 158	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
160		eqid	⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
161	7 9 160	zndvds0	⊢ ( ( 𝑃 ∈ ℕ0 ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑃 ∥ ( 2 · 𝑥 ) ) )
162	108 65 161	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑃 ∥ ( 2 · 𝑥 ) ) )
163	162	necon3abid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g ‘ 𝑌 ) ↔ ¬ 𝑃 ∥ ( 2 · 𝑥 ) ) )
164	159 163	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g ‘ 𝑌 ) )
165	20	simplbi	⊢ ( 𝑌 ∈ Field → 𝑌 ∈ DivRing )
166	19 165	syl	⊢ ( 𝜑 → 𝑌 ∈ DivRing )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑌 ∈ DivRing )
168	14 134 160	drngunit	⊢ ( 𝑌 ∈ DivRing → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) ↔ ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g ‘ 𝑌 ) ) ) )
169	167 168	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) ↔ ( ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ≠ ( 0g ‘ 𝑌 ) ) ) )
170	121 164 169	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ ( Unit ‘ 𝑌 ) )
171	170	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Unit ‘ 𝑌 ) )
172		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 2 · 𝑥 ) ) ∈ V )
173	130 25 172 42	fsuppmptdm	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) finSupp ( 0g ‘ 𝐺 ) )
174	16 24 25 136 171 173	gsumsubmcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) )
175		eqid	⊢ ( /r ‘ 𝑌 ) = ( /r ‘ 𝑌 )
176		eqid	⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
177	134 175 176	dvrid	⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) ) → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 1r ‘ 𝑌 ) )
178	27 174 177	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 1r ‘ 𝑌 ) )
179	120	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( Base ‘ 𝑌 ) )
180		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ∈ V )
181	129 25 180 42	fsuppmptdm	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) finSupp ( 0g ‘ 𝐺 ) )
182	15 16 24 25 179 181	gsumcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
183	14 134 175 114	dvrcan3	⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ∈ ( Unit ‘ 𝑌 ) ) → ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) )
184	27 182 174 183	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) ( .r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) ( /r ‘ 𝑌 ) ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 2 · 𝑥 ) ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) )
185	133 178 184	3eqtr3rd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( ( - 1 ↑ 𝑅 ) · 𝑄 ) ) ) ) = ( 1r ‘ 𝑌 ) )