Theorem lgsqrlem1

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	lgsqr.y	$$⊢Y=\mathbb{Z}/P\mathbb{Z}$$
	lgsqr.s	$$⊢S={\mathrm{Poly}}_1\left(Y\right)$$
	lgsqr.b	$$⊢B={\mathrm{Base}}_S$$
	lgsqr.d	$$⊢D={\mathrm{deg}}_1\left(Y\right)$$
	lgsqr.o	$$⊢O={\mathrm{eval}}_1\left(Y\right)$$
	lgsqr.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	lgsqr.x	$$⊢X={\mathrm{var}}_1\left(Y\right)$$
	lgsqr.m	$$⊢\underset{\dot{}}{-}={-}_S$$
	lgsqr.u	$$⊢\underset{\dot{}}{1}=1_S$$
	lgsqr.t	$$⊢T=\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}$$
	lgsqr.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
	lgsqr.1	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
	lgsqrlem1.3	$$⊢\phi \to A\in \mathbb{Z}$$
	lgsqrlem1.4	$$⊢\phi \to A^{\frac{P-1}{2}}\mathrm{mod}P=1\mathrm{mod}P$$
Assertion	lgsqrlem1	$$⊢\phi \to O\left(T\right)\left(L\left(A\right)\right)=0_Y$$

Proof

Step	Hyp	Ref	Expression
1		lgsqr.y	$$⊢Y=\mathbb{Z}/P\mathbb{Z}$$
2		lgsqr.s	$$⊢S={\mathrm{Poly}}_1\left(Y\right)$$
3		lgsqr.b	$$⊢B={\mathrm{Base}}_S$$
4		lgsqr.d	$$⊢D={\mathrm{deg}}_1\left(Y\right)$$
5		lgsqr.o	$$⊢O={\mathrm{eval}}_1\left(Y\right)$$
6		lgsqr.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
7		lgsqr.x	$$⊢X={\mathrm{var}}_1\left(Y\right)$$
8		lgsqr.m	$$⊢\underset{\dot{}}{-}={-}_S$$
9		lgsqr.u	$$⊢\underset{\dot{}}{1}=1_S$$
10		lgsqr.t	$$⊢T=\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}$$
11		lgsqr.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
12		lgsqr.1	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
13		lgsqrlem1.3	$$⊢\phi \to A\in \mathbb{Z}$$
14		lgsqrlem1.4	$$⊢\phi \to A^{\frac{P-1}{2}}\mathrm{mod}P=1\mathrm{mod}P$$
15	10	fveq2i	$$⊢O\left(T\right)=O\left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\right)$$
16	15	fveq1i	$$⊢O\left(T\right)\left(L\left(A\right)\right)=O\left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)$$
17		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
18	12	eldifad	$$⊢\phi \to P\in \mathbb{P}$$
19	1	znfld	$$⊢P\in \mathbb{P}\to Y\in \mathrm{Field}$$
20	18 19	syl	$$⊢\phi \to Y\in \mathrm{Field}$$
21		fldidom	$$⊢Y\in \mathrm{Field}\to Y\in \mathrm{IDomn}$$
22	20 21	syl	$$⊢\phi \to Y\in \mathrm{IDomn}$$
23		isidom	$$⊢Y\in \mathrm{IDomn}\leftrightarrow \left(Y\in \mathrm{CRing}\wedge Y\in \mathrm{Domn}\right)$$
24	23	simplbi	$$⊢Y\in \mathrm{IDomn}\to Y\in \mathrm{CRing}$$
25	22 24	syl	$$⊢\phi \to Y\in \mathrm{CRing}$$
26		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
27	25 26	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
28	11	zrhrhm	$$⊢Y\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
29	27 28	syl	$$⊢\phi \to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
30		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
31	30 17	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_Y$$
32	29 31	syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_Y$$
33	32 13	ffvelrnd	$$⊢\phi \to L\left(A\right)\in {\mathrm{Base}}_Y$$
34	5 7 17 2 3 25 33	evl1vard	$$⊢\phi \to \left(X\in B\wedge O\left(X\right)\left(L\left(A\right)\right)=L\left(A\right)\right)$$
35		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Y}={\cdot }_{{\mathrm{mulGrp}}_Y}$$
36		oddprm	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \frac{P-1}{2}\in \mathbb{N}$$
37	12 36	syl	$$⊢\phi \to \frac{P-1}{2}\in \mathbb{N}$$
38	37	nnnn0d	$$⊢\phi \to \frac{P-1}{2}\in {\mathbb{N}}_0$$
39	5 2 17 3 25 33 34 6 35 38	evl1expd	$$⊢\phi \to \left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B\wedge O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=\left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)\right)$$
40		zringmpg	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
41		eqid	$$⊢{\mathrm{mulGrp}}_Y={\mathrm{mulGrp}}_Y$$
42	40 41	rhmmhm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)$$
43	29 42	syl	$$⊢\phi \to L\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)$$
44	40 30	mgpbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
45		eqid	$$⊢{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}={\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
46	44 45 35	mhmmulg	$$⊢\left(L\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)\wedge \frac{P-1}{2}\in {\mathbb{N}}_0\wedge A\in \mathbb{Z}\right)\to L\left(\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A\right)=\left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)$$
47	43 38 13 46	syl3anc	$$⊢\phi \to L\left(\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A\right)=\left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)$$
48		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
49		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
50	49	subrgsubm	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
51	48 50	mp1i	$$⊢\phi \to \mathbb{Z}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
52		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
53		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
54	52 53 45	submmulg	$$⊢\left(\mathbb{Z}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \frac{P-1}{2}\in {\mathbb{N}}_0\wedge A\in \mathbb{Z}\right)\to \left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A$$
55	51 38 13 54	syl3anc	$$⊢\phi \to \left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A$$
56	13	zcnd	$$⊢\phi \to A\in ℂ$$
57		cnfldexp	$$⊢\left(A\in ℂ\wedge \frac{P-1}{2}\in {\mathbb{N}}_0\right)\to \left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{\frac{P-1}{2}}$$
58	56 38 57	syl2anc	$$⊢\phi \to \left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{\frac{P-1}{2}}$$
59	55 58	eqtr3d	$$⊢\phi \to \left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A=A^{\frac{P-1}{2}}$$
60	59	fveq2d	$$⊢\phi \to L\left(\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A\right)=L\left(A^{\frac{P-1}{2}}\right)$$
61		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
62	18 61	syl	$$⊢\phi \to P\in \mathbb{N}$$
63		zexpcl	$$⊢\left(A\in \mathbb{Z}\wedge \frac{P-1}{2}\in {\mathbb{N}}_0\right)\to A^{\frac{P-1}{2}}\in \mathbb{Z}$$
64	13 38 63	syl2anc	$$⊢\phi \to A^{\frac{P-1}{2}}\in \mathbb{Z}$$
65		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
66		moddvds	$$⊢\left(P\in \mathbb{N}\wedge A^{\frac{P-1}{2}}\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(A^{\frac{P-1}{2}}\mathrm{mod}P=1\mathrm{mod}P\leftrightarrow P\parallel \left(A^{\frac{P-1}{2}}-1\right)\right)$$
67	62 64 65 66	syl3anc	$$⊢\phi \to \left(A^{\frac{P-1}{2}}\mathrm{mod}P=1\mathrm{mod}P\leftrightarrow P\parallel \left(A^{\frac{P-1}{2}}-1\right)\right)$$
68	14 67	mpbid	$$⊢\phi \to P\parallel \left(A^{\frac{P-1}{2}}-1\right)$$
69	62	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
70	1 11	zndvds	$$⊢\left(P\in {\mathbb{N}}_0\wedge A^{\frac{P-1}{2}}\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(L\left(A^{\frac{P-1}{2}}\right)=L\left(1\right)\leftrightarrow P\parallel \left(A^{\frac{P-1}{2}}-1\right)\right)$$
71	69 64 65 70	syl3anc	$$⊢\phi \to \left(L\left(A^{\frac{P-1}{2}}\right)=L\left(1\right)\leftrightarrow P\parallel \left(A^{\frac{P-1}{2}}-1\right)\right)$$
72	68 71	mpbird	$$⊢\phi \to L\left(A^{\frac{P-1}{2}}\right)=L\left(1\right)$$
73		zring1	$$⊢1=1_{{\mathbb{Z}}_{\mathrm{ring}}}$$
74		eqid	$$⊢1_Y=1_Y$$
75	73 74	rhm1	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L\left(1\right)=1_Y$$
76	29 75	syl	$$⊢\phi \to L\left(1\right)=1_Y$$
77	60 72 76	3eqtrd	$$⊢\phi \to L\left(\left(\frac{P-1}{2}\right){\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}A\right)=1_Y$$
78	47 77	eqtr3d	$$⊢\phi \to \left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)=1_Y$$
79	78	eqeq2d	$$⊢\phi \to \left(O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=\left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)\leftrightarrow O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=1_Y\right)$$
80	79	anbi2d	$$⊢\phi \to \left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B\wedge O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=\left(\frac{P-1}{2}\right){\cdot }_{{\mathrm{mulGrp}}_Y}L\left(A\right)\right)\leftrightarrow \left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B\wedge O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=1_Y\right)\right)$$
81	39 80	mpbid	$$⊢\phi \to \left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B\wedge O\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\left(L\left(A\right)\right)=1_Y\right)$$
82		eqid	$$⊢\mathrm{algSc}\left(S\right)=\mathrm{algSc}\left(S\right)$$
83	17 74	ringidcl	$$⊢Y\in \mathrm{Ring}\to 1_Y\in {\mathrm{Base}}_Y$$
84	27 83	syl	$$⊢\phi \to 1_Y\in {\mathrm{Base}}_Y$$
85	5 2 17 82 3 25 84 33	evl1scad	$$⊢\phi \to \left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\in B\wedge O\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\right)\left(L\left(A\right)\right)=1_Y\right)$$
86	2 82 74 9	ply1scl1	$$⊢Y\in \mathrm{Ring}\to \mathrm{algSc}\left(S\right)\left(1_Y\right)=\underset{\dot{}}{1}$$
87	27 86	syl	$$⊢\phi \to \mathrm{algSc}\left(S\right)\left(1_Y\right)=\underset{\dot{}}{1}$$
88	87	eleq1d	$$⊢\phi \to \left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\in B\leftrightarrow \underset{\dot{}}{1}\in B\right)$$
89	87	fveq2d	$$⊢\phi \to O\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\right)=O\left(\underset{\dot{}}{1}\right)$$
90	89	fveq1d	$$⊢\phi \to O\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\right)\left(L\left(A\right)\right)=O\left(\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)$$
91	90	eqeq1d	$$⊢\phi \to \left(O\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\right)\left(L\left(A\right)\right)=1_Y\leftrightarrow O\left(\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)=1_Y\right)$$
92	88 91	anbi12d	$$⊢\phi \to \left(\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\in B\wedge O\left(\mathrm{algSc}\left(S\right)\left(1_Y\right)\right)\left(L\left(A\right)\right)=1_Y\right)\leftrightarrow \left(\underset{\dot{}}{1}\in B\wedge O\left(\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)=1_Y\right)\right)$$
93	85 92	mpbid	$$⊢\phi \to \left(\underset{\dot{}}{1}\in B\wedge O\left(\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)=1_Y\right)$$
94		eqid	$$⊢{-}_Y={-}_Y$$
95	5 2 17 3 25 33 81 93 8 94	evl1subd	$$⊢\phi \to \left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\in B\wedge O\left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)=1_Y{-}_Y{1}_Y\right)$$
96	95	simprd	$$⊢\phi \to O\left(\left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\right)\left(L\left(A\right)\right)=1_Y{-}_Y{1}_Y$$
97	16 96	eqtrid	$$⊢\phi \to O\left(T\right)\left(L\left(A\right)\right)=1_Y{-}_Y{1}_Y$$
98		ringgrp	$$⊢Y\in \mathrm{Ring}\to Y\in \mathrm{Grp}$$
99	27 98	syl	$$⊢\phi \to Y\in \mathrm{Grp}$$
100		eqid	$$⊢0_Y=0_Y$$
101	17 100 94	grpsubid	$$⊢\left(Y\in \mathrm{Grp}\wedge 1_Y\in {\mathrm{Base}}_Y\right)\to 1_Y{-}_Y{1}_Y=0_Y$$
102	99 84 101	syl2anc	$$⊢\phi \to 1_Y{-}_Y{1}_Y=0_Y$$
103	97 102	eqtrd	$$⊢\phi \to O\left(T\right)\left(L\left(A\right)\right)=0_Y$$