Theorem vr1nz

Description: A univariate polynomial variable cannot be the zero polynomial. (Contributed by Thierry Arnoux, 14-Nov-2025)

	Ref	Expression
Hypotheses	vr1nz.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
	vr1nz.z	$$⊢Z=0_P$$
	vr1nz.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	vr1nz.p	$$⊢P={\mathrm{Poly}}_1\left(U\right)$$
	vr1nz.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	vr1nz.1	$$⊢\phi \to S\in \mathrm{NzRing}$$
	vr1nz.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
Assertion	vr1nz	$$⊢\phi \to X\ne Z$$

Proof

Step	Hyp	Ref	Expression
1		vr1nz.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
2		vr1nz.z	$$⊢Z=0_P$$
3		vr1nz.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		vr1nz.p	$$⊢P={\mathrm{Poly}}_1\left(U\right)$$
5		vr1nz.s	$$⊢\phi \to S\in \mathrm{CRing}$$
6		vr1nz.1	$$⊢\phi \to S\in \mathrm{NzRing}$$
7		vr1nz.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8		eqid	$$⊢1_S=1_S$$
9		eqid	$$⊢0_S=0_S$$
10	8 9	nzrnz	$$⊢S\in \mathrm{NzRing}\to 1_S\ne 0_S$$
11	6 10	syl	$$⊢\phi \to 1_S\ne 0_S$$
12	5	crnggrpd	$$⊢\phi \to S\in \mathrm{Grp}$$
13	12	grpmndd	$$⊢\phi \to S\in \mathrm{Mnd}$$
14		subrgsubg	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\in \mathrm{SubGrp}\left(S\right)$$
15	9	subg0cl	$$⊢R\in \mathrm{SubGrp}\left(S\right)\to 0_S\in R$$
16	7 14 15	3syl	$$⊢\phi \to 0_S\in R$$
17		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
18	17	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq {\mathrm{Base}}_S$$
19	7 18	syl	$$⊢\phi \to R\subseteq {\mathrm{Base}}_S$$
20	3 17 9	ress0g	$$⊢\left(S\in \mathrm{Mnd}\wedge 0_S\in R\wedge R\subseteq {\mathrm{Base}}_S\right)\to 0_S=0_U$$
21	13 16 19 20	syl3anc	$$⊢\phi \to 0_S=0_U$$
22	21	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(0_S\right)=\mathrm{algSc}\left(P\right)\left(0_U\right)$$
23	22	fveq2d	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)=\left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_U\right)\right)$$
24	23	adantr	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)=\left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_U\right)\right)$$
25	3	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
26		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
27		eqid	$$⊢0_U=0_U$$
28	4 26 27 2	ply1scl0	$$⊢U\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(0_U\right)=Z$$
29	7 25 28	3syl	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(0_U\right)=Z$$
30	29	adantr	$$⊢\left(\phi \wedge X=Z\right)\to \mathrm{algSc}\left(P\right)\left(0_U\right)=Z$$
31		simpr	$$⊢\left(\phi \wedge X=Z\right)\to X=Z$$
32	30 31	eqtr4d	$$⊢\left(\phi \wedge X=Z\right)\to \mathrm{algSc}\left(P\right)\left(0_U\right)=X$$
33	32	fveq2d	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_U\right)\right)=\left(S{\mathrm{evalSub}}_{1}R\right)\left(X\right)$$
34		eqid	$$⊢S{\mathrm{evalSub}}_{1}R=S{\mathrm{evalSub}}_{1}R$$
35	34 1 3 17 5 7	evls1var	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}R\right)\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}$$
36	35	adantr	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}$$
37	24 33 36	3eqtrd	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}$$
38	37	fveq1d	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)\left(1_S\right)=\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}\right)\left(1_S\right)$$
39	5	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
40	17 8 39	ringidcld	$$⊢\phi \to 1_S\in {\mathrm{Base}}_S$$
41	34 4 3 17 26 5 7 16 40	evls1scafv	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)\left(1_S\right)=0_S$$
42	41	adantr	$$⊢\left(\phi \wedge X=Z\right)\to \left(S{\mathrm{evalSub}}_{1}R\right)\left(\mathrm{algSc}\left(P\right)\left(0_S\right)\right)\left(1_S\right)=0_S$$
43		fvresi	$$⊢1_S\in {\mathrm{Base}}_S\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}\right)\left(1_S\right)=1_S$$
44	40 43	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}\right)\left(1_S\right)=1_S$$
45	44	adantr	$$⊢\left(\phi \wedge X=Z\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_S}\right)\left(1_S\right)=1_S$$
46	38 42 45	3eqtr3rd	$$⊢\left(\phi \wedge X=Z\right)\to 1_S=0_S$$
47	11 46	mteqand	$$⊢\phi \to X\ne Z$$