Theorem evls1degle1

Description: Evaluation of a univariate polynomial of degree at most 1. (Contributed by Thierry Arnoux, 8-Nov-2026)

	Ref	Expression
Hypotheses	evls1degle1.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	evls1degle1.q	$$⊢Q=R{\mathrm{evalSub}}_{1}S$$
	evls1degle1.v	$$⊢V={\mathrm{Base}}_R$$
	evls1degle1.u	$$⊢U={\mathrm{Base}}_P$$
	evls1degle1.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	evls1degle1.t	$$⊢\underset{\dot{}}{+}={+}_R$$
	evls1degle1.c	$$⊢C={\mathrm{coe}}_1\left(F\right)$$
	evls1degle1.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	evls1degle1.a	$$⊢A=C\left(1\right)$$
	evls1degle1.b	$$⊢B=C\left(0\right)$$
	evls1degle1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evls1degle1.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	evls1degle1.f	$$⊢\phi \to F\in U$$
	evls1degle1.1	$$⊢\phi \to D\left(F\right)\le 1$$
	evls1degle1.x	$$⊢\phi \to X\in V$$
Assertion	evls1degle1	$$⊢\phi \to Q\left(F\right)\left(X\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$

Proof

Step	Hyp	Ref	Expression
1		evls1degle1.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
2		evls1degle1.q	$$⊢Q=R{\mathrm{evalSub}}_{1}S$$
3		evls1degle1.v	$$⊢V={\mathrm{Base}}_R$$
4		evls1degle1.u	$$⊢U={\mathrm{Base}}_P$$
5		evls1degle1.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		evls1degle1.t	$$⊢\underset{\dot{}}{+}={+}_R$$
7		evls1degle1.c	$$⊢C={\mathrm{coe}}_1\left(F\right)$$
8		evls1degle1.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
9		evls1degle1.a	$$⊢A=C\left(1\right)$$
10		evls1degle1.b	$$⊢B=C\left(0\right)$$
11		evls1degle1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
12		evls1degle1.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
13		evls1degle1.f	$$⊢\phi \to F\in U$$
14		evls1degle1.1	$$⊢\phi \to D\left(F\right)\le 1$$
15		evls1degle1.x	$$⊢\phi \to X\in V$$
16		eqid	$$⊢0_R=0_R$$
17	11	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
18	17	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to R\in \mathrm{Ring}$$
19	18	ringgrpd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to R\in \mathrm{Grp}$$
20	3	subrgss	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S\subseteq V$$
21	12 20	syl	$$⊢\phi \to S\subseteq V$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
24	7 4 1 23	coe1fvalcl	$$⊢\left(F\in U\wedge 0\in {\mathbb{N}}_0\right)\to C\left(0\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
25	13 22 24	sylancl	$$⊢\phi \to C\left(0\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
26		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
27	26	subrgbas	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
28	12 27	syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
29	25 28	eleqtrrd	$$⊢\phi \to C\left(0\right)\in S$$
30	10 29	eqeltrid	$$⊢\phi \to B\in S$$
31	21 30	sseldd	$$⊢\phi \to B\in V$$
32	31	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to B\in V$$
33	3 6 16 19 32	grplidd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 0_R\underset{\dot{}}{+}B=B$$
34		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
35	34 26 1 4	subrgply1	$$⊢S\in \mathrm{SubRing}\left(R\right)\to U\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
36		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
37	36	subrgss	$$⊢U\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)\to U\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
38	12 35 37	3syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
39	38 13	sseldd	$$⊢\phi \to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
40	39	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
41		1nn0	$$⊢1\in {\mathbb{N}}_0$$
42	41	a1i	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 1\in {\mathbb{N}}_0$$
43	8 34 36	deg1xrcl	$$⊢F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to D\left(F\right)\in {ℝ}^{*}$$
44	39 43	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
45	44	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to D\left(F\right)\in {ℝ}^{*}$$
46		0xr	$$⊢0\in {ℝ}^{*}$$
47	46	a1i	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 0\in {ℝ}^{*}$$
48		1xr	$$⊢1\in {ℝ}^{*}$$
49	48	a1i	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 1\in {ℝ}^{*}$$
50		simpr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to D\left(F\right)\le 0$$
51		0lt1	$$⊢0<1$$
52	51	a1i	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 0<1$$
53	45 47 49 50 52	xrlelttrd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to D\left(F\right)<1$$
54	8 34 36 16 7	deg1lt	$$⊢\left(F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge 1\in {\mathbb{N}}_0\wedge D\left(F\right)<1\right)\to C\left(1\right)=0_R$$
55	40 42 53 54	syl3anc	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to C\left(1\right)=0_R$$
56	9 55	eqtrid	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to A=0_R$$
57	56	oveq1d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to A\underset{\dot{}}{·}X=0_R\underset{\dot{}}{·}X$$
58	15	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to X\in V$$
59	3 5 16 18 58	ringlzd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to 0_R\underset{\dot{}}{·}X=0_R$$
60	57 59	eqtrd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to A\underset{\dot{}}{·}X=0_R$$
61	60	oveq1d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B=0_R\underset{\dot{}}{+}B$$
62		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
63	8 34 36 62	deg1le0	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to \left(D\left(F\right)\le 0\leftrightarrow F=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)\right)$$
64	63	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\wedge D\left(F\right)\le 0\right)\to F=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
65	18 40 50 64	syl21anc	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to F=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
66	7	fveq1i	$$⊢C\left(0\right)={\mathrm{coe}}_1\left(F\right)\left(0\right)$$
67	10 66	eqtri	$$⊢B={\mathrm{coe}}_1\left(F\right)\left(0\right)$$
68	67	fveq2i	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
69	65 68	eqtr4di	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to F=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)$$
70	69	fveq2d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(F\right)=Q\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)\right)$$
71	70	fveq1d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(F\right)\left(X\right)=Q\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)\right)\left(X\right)$$
72	12	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to S\in \mathrm{SubRing}\left(R\right)$$
73		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
74	34 62 26 1 72 73	subrg1ascl	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to \mathrm{algSc}\left(P\right)={\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\upharpoonright }_S$$
75	74	fveq1d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to \mathrm{algSc}\left(P\right)\left(B\right)=\left({\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\upharpoonright }_S\right)\left(B\right)$$
76	30	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to B\in S$$
77	76	fvresd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to \left({\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\upharpoonright }_S\right)\left(B\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)$$
78	75 77	eqtr2d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)=\mathrm{algSc}\left(P\right)\left(B\right)$$
79	78	fveq2d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)\right)=Q\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)$$
80	79	fveq1d	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(B\right)\right)\left(X\right)=Q\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\left(X\right)$$
81	11	adantr	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to R\in \mathrm{CRing}$$
82	2 1 26 3 73 81 72 76 58	evls1scafv	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\left(X\right)=B$$
83	71 80 82	3eqtrd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(F\right)\left(X\right)=B$$
84	33 61 83	3eqtr4rd	$$⊢\left(\phi \wedge D\left(F\right)\le 0\right)\to Q\left(F\right)\left(X\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
85		eqid	$$⊢{\mathrm{eval}}_1\left(R\right)={\mathrm{eval}}_1\left(R\right)$$
86	2 3 1 26 4 85 11 12	ressply1evl	$$⊢\phi \to Q={{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U$$
87	86	fveq1d	$$⊢\phi \to Q\left(F\right)=\left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U\right)\left(F\right)$$
88	13	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U\right)\left(F\right)={\mathrm{eval}}_1\left(R\right)\left(F\right)$$
89	87 88	eqtrd	$$⊢\phi \to Q\left(F\right)={\mathrm{eval}}_1\left(R\right)\left(F\right)$$
90	89	fveq1d	$$⊢\phi \to Q\left(F\right)\left(X\right)={\mathrm{eval}}_1\left(R\right)\left(F\right)\left(X\right)$$
91	90	adantr	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to Q\left(F\right)\left(X\right)={\mathrm{eval}}_1\left(R\right)\left(F\right)\left(X\right)$$
92	11	adantr	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to R\in \mathrm{CRing}$$
93	39	adantr	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
94		simpr	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to D\left(F\right)=1$$
95	15	adantr	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to X\in V$$
96	34 85 3 36 5 6 7 8 9 10 92 93 94 95	evl1deg1	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to {\mathrm{eval}}_1\left(R\right)\left(F\right)\left(X\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
97	91 96	eqtrd	$$⊢\left(\phi \wedge D\left(F\right)=1\right)\to Q\left(F\right)\left(X\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
98	8 34 36 39 14	deg1le1	$$⊢\phi \to \left(D\left(F\right)\le 0\vee D\left(F\right)=1\right)$$
99	84 97 98	mpjaodan	$$⊢\phi \to Q\left(F\right)\left(X\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$