Theorem lgsqrlem3

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)$$
	lgsqr.g	$$⊢G=\left(y\in \left(1\dots \frac{P-1}{2}\right)⟼L\left(y^2\right)\right)$$
	lgsqr.3	$$⊢\phi \to A\in \mathbb{Z}$$
	lgsqr.4	$$⊢\phi \to A{/}_{L}P=1$$
Assertion	lgsqrlem3	$$⊢\phi \to L\left(A\right)\in {O\left(T\right)}^{-1}\left[\left\{0_Y\right\}\right]$$

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		lgsqr.g	$$⊢G=\left(y\in \left(1\dots \frac{P-1}{2}\right)⟼L\left(y^2\right)\right)$$
14		lgsqr.3	$$⊢\phi \to A\in \mathbb{Z}$$
15		lgsqr.4	$$⊢\phi \to A{/}_{L}P=1$$
16	12	eldifad	$$⊢\phi \to P\in \mathbb{P}$$
17	1	znfld	$$⊢P\in \mathbb{P}\to Y\in \mathrm{Field}$$
18	16 17	syl	$$⊢\phi \to Y\in \mathrm{Field}$$
19		fldidom	$$⊢Y\in \mathrm{Field}\to Y\in \mathrm{IDomn}$$
20	18 19	syl	$$⊢\phi \to Y\in \mathrm{IDomn}$$
21		isidom	$$⊢Y\in \mathrm{IDomn}\leftrightarrow \left(Y\in \mathrm{CRing}\wedge Y\in \mathrm{Domn}\right)$$
22	21	simplbi	$$⊢Y\in \mathrm{IDomn}\to Y\in \mathrm{CRing}$$
23	20 22	syl	$$⊢\phi \to Y\in \mathrm{CRing}$$
24		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
25	23 24	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
26	11	zrhrhm	$$⊢Y\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
27	25 26	syl	$$⊢\phi \to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
28		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
29		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
30	28 29	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_Y$$
31	27 30	syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_Y$$
32	31 14	ffvelcdmd	$$⊢\phi \to L\left(A\right)\in {\mathrm{Base}}_Y$$
33		lgsvalmod	$$⊢\left(A\in \mathbb{Z}\wedge P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\right)\to \left(A{/}_{L}P\right)\mathrm{mod}P=A^{\frac{P-1}{2}}\mathrm{mod}P$$
34	14 12 33	syl2anc	$$⊢\phi \to \left(A{/}_{L}P\right)\mathrm{mod}P=A^{\frac{P-1}{2}}\mathrm{mod}P$$
35	15	oveq1d	$$⊢\phi \to \left(A{/}_{L}P\right)\mathrm{mod}P=1\mathrm{mod}P$$
36	34 35	eqtr3d	$$⊢\phi \to A^{\frac{P-1}{2}}\mathrm{mod}P=1\mathrm{mod}P$$
37	1 2 3 4 5 6 7 8 9 10 11 12 14 36	lgsqrlem1	$$⊢\phi \to O\left(T\right)\left(L\left(A\right)\right)=0_Y$$
38		eqid	$$⊢Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y=Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y$$
39		eqid	$$⊢{\mathrm{Base}}_{\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)}={\mathrm{Base}}_{\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)}$$
40		fvexd	$$⊢\phi \to {\mathrm{Base}}_Y\in \mathrm{V}$$
41	5 2 38 29	evl1rhm	$$⊢Y\in \mathrm{CRing}\to O\in \left(S\mathrm{RingHom}\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)\right)$$
42	23 41	syl	$$⊢\phi \to O\in \left(S\mathrm{RingHom}\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)\right)$$
43	3 39	rhmf	$$⊢O\in \left(S\mathrm{RingHom}\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)\right)\to O:B⟶{\mathrm{Base}}_{\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)}$$
44	42 43	syl	$$⊢\phi \to O:B⟶{\mathrm{Base}}_{\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)}$$
45	2	ply1ring	$$⊢Y\in \mathrm{Ring}\to S\in \mathrm{Ring}$$
46	25 45	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
47		ringgrp	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Grp}$$
48	46 47	syl	$$⊢\phi \to S\in \mathrm{Grp}$$
49		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
50	49 3	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
51	49	ringmgp	$$⊢S\in \mathrm{Ring}\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
52	46 51	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
53		oddprm	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \frac{P-1}{2}\in \mathbb{N}$$
54	12 53	syl	$$⊢\phi \to \frac{P-1}{2}\in \mathbb{N}$$
55	54	nnnn0d	$$⊢\phi \to \frac{P-1}{2}\in {\mathbb{N}}_0$$
56	7 2 3	vr1cl	$$⊢Y\in \mathrm{Ring}\to X\in B$$
57	25 56	syl	$$⊢\phi \to X\in B$$
58	50 6 52 55 57	mulgnn0cld	$$⊢\phi \to \left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B$$
59	3 9	ringidcl	$$⊢S\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
60	46 59	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
61	3 8	grpsubcl	$$⊢\left(S\in \mathrm{Grp}\wedge \left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\in B\wedge \underset{\dot{}}{1}\in B\right)\to \left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\in B$$
62	48 58 60 61	syl3anc	$$⊢\phi \to \left(\left(\frac{P-1}{2}\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\in B$$
63	10 62	eqeltrid	$$⊢\phi \to T\in B$$
64	44 63	ffvelcdmd	$$⊢\phi \to O\left(T\right)\in {\mathrm{Base}}_{\left(Y{\uparrow }_{𝑠}{\mathrm{Base}}_Y\right)}$$
65	38 29 39 18 40 64	pwselbas	$$⊢\phi \to O\left(T\right):{\mathrm{Base}}_Y⟶{\mathrm{Base}}_Y$$
66	65	ffnd	$$⊢\phi \to O\left(T\right)Fn{\mathrm{Base}}_Y$$
67		fniniseg	$$⊢O\left(T\right)Fn{\mathrm{Base}}_Y\to \left(L\left(A\right)\in {O\left(T\right)}^{-1}\left[\left\{0_Y\right\}\right]\leftrightarrow \left(L\left(A\right)\in {\mathrm{Base}}_Y\wedge O\left(T\right)\left(L\left(A\right)\right)=0_Y\right)\right)$$
68	66 67	syl	$$⊢\phi \to \left(L\left(A\right)\in {O\left(T\right)}^{-1}\left[\left\{0_Y\right\}\right]\leftrightarrow \left(L\left(A\right)\in {\mathrm{Base}}_Y\wedge O\left(T\right)\left(L\left(A\right)\right)=0_Y\right)\right)$$
69	32 37 68	mpbir2and	$$⊢\phi \to L\left(A\right)\in {O\left(T\right)}^{-1}\left[\left\{0_Y\right\}\right]$$