Theorem vr1nz

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

	Ref	Expression
Hypotheses	vr1nz.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
	vr1nz.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	vr1nz.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	vr1nz.p	⊢ 𝑃 = ( Poly1 ‘ 𝑈 )
	vr1nz.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	vr1nz.1	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
	vr1nz.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion	vr1nz	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		vr1nz.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
2		vr1nz.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
3		vr1nz.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		vr1nz.p	⊢ 𝑃 = ( Poly1 ‘ 𝑈 )
5		vr1nz.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
6		vr1nz.1	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
7		vr1nz.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
9		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
10	8 9	nzrnz	⊢ ( 𝑆 ∈ NzRing → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
11	6 10	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
12	5	crnggrpd	⊢ ( 𝜑 → 𝑆 ∈ Grp )
13	12	grpmndd	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
14		subrgsubg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ ( SubGrp ‘ 𝑆 ) )
15	9	subg0cl	⊢ ( 𝑅 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
16	7 14 15	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
17		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18	17	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
19	7 18	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
20	3 17 9	ress0g	⊢ ( ( 𝑆 ∈ Mnd ∧ ( 0g ‘ 𝑆 ) ∈ 𝑅 ∧ 𝑅 ⊆ ( Base ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
21	13 16 19 20	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
22	21	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) )
25	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
26		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
27		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
28	4 26 27 2	ply1scl0	⊢ ( 𝑈 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
29	7 25 28	3syl	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → 𝑋 = 𝑍 )
32	30 31	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑋 )
33	32	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) )
34		eqid	⊢ ( 𝑆 evalSub1 𝑅 ) = ( 𝑆 evalSub1 𝑅 )
35	34 1 3 17 5 7	evls1var	⊢ ( 𝜑 → ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
37	24 33 36	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
38	37	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) )
39	5	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
40	17 8 39	ringidcld	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
41	34 4 3 17 26 5 7 16 40	evls1scafv	⊢ ( 𝜑 → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
43		fvresi	⊢ ( ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
44	40 43	syl	⊢ ( 𝜑 → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
46	38 42 45	3eqtr3rd	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) )
47	11 46	mteqand	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )