Metamath Proof Explorer

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 ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
evls1degle1.q ⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
evls1degle1.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
evls1degle1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evls1degle1.m ⊢ · = ( .r ‘ 𝑅 )
evls1degle1.t ⊢ + = ( +g ‘ 𝑅 )
evls1degle1.c ⊢ 𝐶 = ( coe1 ‘ 𝐹 )
evls1degle1.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
evls1degle1.a ⊢ 𝐴 = ( 𝐶 ‘ 1 )
evls1degle1.b ⊢ 𝐵 = ( 𝐶 ‘ 0 )
evls1degle1.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evls1degle1.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
evls1degle1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
evls1degle1.1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 1 )
evls1degle1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion evls1degle1 ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 evls1degle1.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
2 evls1degle1.q ⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
3 evls1degle1.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
4 evls1degle1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
5 evls1degle1.m ⊢ · = ( .r ‘ 𝑅 )
6 evls1degle1.t ⊢ + = ( +g ‘ 𝑅 )
7 evls1degle1.c ⊢ 𝐶 = ( coe1 ‘ 𝐹 )
8 evls1degle1.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
9 evls1degle1.a ⊢ 𝐴 = ( 𝐶 ‘ 1 )
10 evls1degle1.b ⊢ 𝐵 = ( 𝐶 ‘ 0 )
11 evls1degle1.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
12 evls1degle1.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
13 evls1degle1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
14 evls1degle1.1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 1 )
15 evls1degle1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 11 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝑅 ∈ Ring )
19 18 ringgrpd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝑅 ∈ Grp )
20 3 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝑉 )
21 12 20 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
22 0nn0 ⊢ 0 ∈ ℕ0
23 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
24 7 4 1 23 coe1fvalcl ⊢ ( ( 𝐹 ∈ 𝑈 ∧ 0 ∈ ℕ0 ) → ( 𝐶 ‘ 0 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
25 13 22 24 sylancl ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
26 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
27 26 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
28 12 27 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
29 25 28 eleqtrrd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ 𝑆 )
30 10 29 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
31 21 30 sseldd ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐵 ∈ 𝑉 )
33 3 6 16 19 32 grplidd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 0g ‘ 𝑅 ) + 𝐵 ) = 𝐵 )
34 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
35 34 26 1 4 subrgply1 ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑅 ) ) )
36 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
37 36 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑅 ) ) → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
38 12 35 37 3syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
39 38 13 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
41 1nn0 ⊢ 1 ∈ ℕ0
42 41 a1i ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 1 ∈ ℕ0 )
43 8 34 36 deg1xrcl ⊢ ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
44 39 43 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
46 0xr ⊢ 0 ∈ ℝ*
47 46 a1i ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 0 ∈ ℝ* )
48 1xr ⊢ 1 ∈ ℝ*
49 48 a1i ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 1 ∈ ℝ* )
50 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐷 ‘ 𝐹 ) ≤ 0 )
51 0lt1 ⊢ 0 < 1
52 51 a1i ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 0 < 1 )
53 45 47 49 50 52 xrlelttrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐷 ‘ 𝐹 ) < 1 )
54 8 34 36 16 7 deg1lt ⊢ ( ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 1 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 1 ) → ( 𝐶 ‘ 1 ) = ( 0g ‘ 𝑅 ) )
55 40 42 53 54 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐶 ‘ 1 ) = ( 0g ‘ 𝑅 ) )
56 9 55 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐴 = ( 0g ‘ 𝑅 ) )
57 56 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐴 · 𝑋 ) = ( ( 0g ‘ 𝑅 ) · 𝑋 ) )
58 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝑋 ∈ 𝑉 )
59 3 5 16 18 58 ringlzd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑅 ) )
60 57 59 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝐴 · 𝑋 ) = ( 0g ‘ 𝑅 ) )
61 60 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝐴 · 𝑋 ) + 𝐵 ) = ( ( 0g ‘ 𝑅 ) + 𝐵 ) )
62 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
63 8 34 36 62 deg1le0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ) )
64 63 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐹 = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
65 18 40 50 64 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐹 = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
66 7 fveq1i ⊢ ( 𝐶 ‘ 0 ) = ( ( coe1 ‘ 𝐹 ) ‘ 0 )
67 10 66 eqtri ⊢ 𝐵 = ( ( coe1 ‘ 𝐹 ) ‘ 0 )
68 67 fveq2i ⊢ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) )
69 65 68 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐹 = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) )
70 69 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝑄 ‘ 𝐹 ) = ( 𝑄 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) ) )
71 70 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) ) ‘ 𝑋 ) )
72 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
73 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
74 34 62 26 1 72 73 subrg1ascl ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( algSc ‘ 𝑃 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) )
75 74 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) = ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝐵 ) )
76 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐵 ∈ 𝑆 )
77 76 fvresd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝐵 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) )
78 75 77 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) )
79 78 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( 𝑄 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) ) = ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) )
80 79 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝐵 ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 𝑋 ) )
81 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝑅 ∈ CRing )
82 2 1 26 3 73 81 72 76 58 evls1scafv ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 𝑋 ) = 𝐵 )
83 71 80 82 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = 𝐵 )
84 33 61 83 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
85 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
86 2 3 1 26 4 85 11 12 ressply1evl ⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) )
87 86 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝐹 ) )
88 13 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝐹 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝐹 ) )
89 87 88 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝐹 ) )
90 89 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( ( eval1 ‘ 𝑅 ) ‘ 𝐹 ) ‘ 𝑋 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( ( eval1 ‘ 𝑅 ) ‘ 𝐹 ) ‘ 𝑋 ) )
92 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → 𝑅 ∈ CRing )
93 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
94 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → ( 𝐷 ‘ 𝐹 ) = 1 )
95 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → 𝑋 ∈ 𝑉 )
96 34 85 3 36 5 6 7 8 9 10 92 93 94 95 evl1deg1 ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → ( ( ( eval1 ‘ 𝑅 ) ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
97 91 96 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
98 8 34 36 39 14 deg1le1 ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )
99 84 97 98 mpjaodan ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )