Theorem irngnminplynz

Description: Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	irngnminplynz.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
	irngnminplynz.e	$$⊢\phi \to E\in \mathrm{Field}$$
	irngnminplynz.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	irngnminplynz.m	No typesetting found for |- M = ( E minPoly F ) with typecode |-
	irngnminplynz.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
Assertion	irngnminplynz	$$⊢\phi \to M\left(A\right)\ne Z$$

Proof

Step	Hyp	Ref	Expression
1		irngnminplynz.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
2		irngnminplynz.e	$$⊢\phi \to E\in \mathrm{Field}$$
3		irngnminplynz.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
4		irngnminplynz.m	Could not format M = ( E minPoly F ) : No typesetting found for |- M = ( E minPoly F ) with typecode |-
5		irngnminplynz.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
6		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
7	3 6	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
8		eqid	$$⊢E{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
9	8	subrgring	$$⊢F\in \mathrm{SubRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}$$
10	7 9	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}$$
11		eqid	$$⊢{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
12	11	ply1ring	$$⊢E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
13	10 12	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
14		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
15		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
16	2	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
17		eqid	$$⊢0_E=0_E$$
18	14 8 15 17 16 7	irngssv	$$⊢\phi \to E\mathrm{IntgRing}F\subseteq {\mathrm{Base}}_E$$
19	18 5	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_E$$
20		eqid	$$⊢\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}=\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
21	14 11 15 16 7 19 17 20	ply1annidl	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
23		eqid	$$⊢\mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)=\mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
24	22 23	lidlss	$$⊢\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
25	21 24	syl	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
26	8	sdrgdrng	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
27	3 26	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
28		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
29	11 28 23	ig1pcl	$$⊢\left(E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\wedge \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\right)\to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
30	27 21 29	syl2anc	$$⊢\phi \to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
31	25 30	sseldd	$$⊢\phi \to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
32		eqid	$$⊢\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
33	14 11 15 2 3 19 17 20 32 28	ply1annig1p	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)$$
34		fveq2	$$⊢q=p\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)$$
35	34	fveq1d	$$⊢q=p\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)$$
36	35	eqeq1d	$$⊢q=p\to \left(\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\leftrightarrow \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)=0_E\right)$$
37		simplr	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)$$
38	37	eldifad	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)$$
39	16	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to E\in \mathrm{CRing}$$
40	7	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to F\in \mathrm{SubRing}\left(E\right)$$
41	14 11 22 16 7	evls1dm	$$⊢\phi \to \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
42	41	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
43	38 42	eleqtrd	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
44	14 11 22 39 40 15 43	evls1fvf	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right):{\mathrm{Base}}_E⟶{\mathrm{Base}}_E$$
45	44	ffnd	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)Fn{\mathrm{Base}}_E$$
46		elpreima	$$⊢\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)Fn{\mathrm{Base}}_E\to \left(A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\leftrightarrow \left(A\in {\mathrm{Base}}_E\wedge \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)\in \left\{0_E\right\}\right)\right)$$
47	46	simplbda	$$⊢\left(\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)Fn{\mathrm{Base}}_E\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)\in \left\{0_E\right\}$$
48	45 47	sylancom	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)\in \left\{0_E\right\}$$
49		elsni	$$⊢\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)\in \left\{0_E\right\}\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)=0_E$$
50	48 49	syl	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)=0_E$$
51	36 38 50	elrabd	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
52		eldifsni	$$⊢p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\to p\ne Z$$
53	37 52	syl	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\ne Z$$
54		eqid	$$⊢{\mathrm{Poly}}_1\left(E\right)={\mathrm{Poly}}_1\left(E\right)$$
55	54 8 11 22 7 1	ressply10g	$$⊢\phi \to Z=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
56	55	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to Z=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
57	53 56	neeqtrd	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to p\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
58		nelsn	$$⊢p\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\to \neg p\in \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
59	57 58	syl	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \neg p\in \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
60		nelne1	$$⊢\left(p\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\wedge \neg p\in \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right)\to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
61	51 59 60	syl2anc	$$⊢\left(\left(\phi \wedge p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)\right)\wedge A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\right)\to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
62	14 1 17 2 3	irngnzply1	$$⊢\phi \to E\mathrm{IntgRing}F=\bigcup _{p\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}}{\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]$$
63	5 62	eleqtrd	$$⊢\phi \to A\in \bigcup _{p\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}}{\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]$$
64		eliun	$$⊢A\in \bigcup _{p\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}}{\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]\leftrightarrow \exists p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]$$
65	63 64	sylib	$$⊢\phi \to \exists p\in \left(\mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)\setminus \left\{Z\right\}\right)A\in {\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)}^{-1}\left[\left\{0_E\right\}\right]$$
66	61 65	r19.29a	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
67	33 66	eqnetrrd	$$⊢\phi \to \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
68		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
69	22 68 32	pidlnzb	$$⊢\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}\wedge {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right)\to \left({idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\leftrightarrow \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right)$$
70	69	biimpar	$$⊢\left(\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}\wedge {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right)\wedge \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right)\to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
71	13 31 67 70	syl21anc	$$⊢\phi \to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
72	14 11 15 2 3 19 17 20 32 28 4	minplyval	$$⊢\phi \to M\left(A\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)$$
73	71 72 55	3netr4d	$$⊢\phi \to M\left(A\right)\ne Z$$