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 
|- P = ( Poly1 ` ( R |`s S ) )
evls1degle1.q 
|- Q = ( R evalSub1 S )
evls1degle1.v 
|- V = ( Base ` R )
evls1degle1.u 
|- U = ( Base ` P )
evls1degle1.m 
|- .x. = ( .r ` R )
evls1degle1.t 
|- .+ = ( +g ` R )
evls1degle1.c 
|- C = ( coe1 ` F )
evls1degle1.d 
|- D = ( deg1 ` R )
evls1degle1.a 
|- A = ( C ` 1 )
evls1degle1.b 
|- B = ( C ` 0 )
evls1degle1.r 
|- ( ph -> R e. CRing )
evls1degle1.s 
|- ( ph -> S e. ( SubRing ` R ) )
evls1degle1.f 
|- ( ph -> F e. U )
evls1degle1.1 
|- ( ph -> ( D ` F ) <_ 1 )
evls1degle1.x 
|- ( ph -> X e. V )
Assertion evls1degle1 
|- ( ph -> ( ( Q ` F ) ` X ) = ( ( A .x. X ) .+ B ) )

Proof

Step Hyp Ref Expression
1 evls1degle1.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
2 evls1degle1.q 
 |-  Q = ( R evalSub1 S )
3 evls1degle1.v 
 |-  V = ( Base ` R )
4 evls1degle1.u 
 |-  U = ( Base ` P )
5 evls1degle1.m 
 |-  .x. = ( .r ` R )
6 evls1degle1.t 
 |-  .+ = ( +g ` R )
7 evls1degle1.c 
 |-  C = ( coe1 ` F )
8 evls1degle1.d 
 |-  D = ( deg1 ` R )
9 evls1degle1.a 
 |-  A = ( C ` 1 )
10 evls1degle1.b 
 |-  B = ( C ` 0 )
11 evls1degle1.r 
 |-  ( ph -> R e. CRing )
12 evls1degle1.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
13 evls1degle1.f 
 |-  ( ph -> F e. U )
14 evls1degle1.1 
 |-  ( ph -> ( D ` F ) <_ 1 )
15 evls1degle1.x 
 |-  ( ph -> X e. V )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 11 crngringd 
 |-  ( ph -> R e. Ring )
18 17 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> R e. Ring )
19 18 ringgrpd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> R e. Grp )
20 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ V )
21 12 20 syl 
 |-  ( ph -> S C_ V )
22 0nn0 
 |-  0 e. NN0
23 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
24 7 4 1 23 coe1fvalcl 
 |-  ( ( F e. U /\ 0 e. NN0 ) -> ( C ` 0 ) e. ( Base ` ( R |`s S ) ) )
25 13 22 24 sylancl 
 |-  ( ph -> ( C ` 0 ) e. ( Base ` ( R |`s S ) ) )
26 eqid 
 |-  ( R |`s S ) = ( R |`s S )
27 26 subrgbas 
 |-  ( S e. ( SubRing ` R ) -> S = ( Base ` ( R |`s S ) ) )
28 12 27 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
29 25 28 eleqtrrd 
 |-  ( ph -> ( C ` 0 ) e. S )
30 10 29 eqeltrid 
 |-  ( ph -> B e. S )
31 21 30 sseldd 
 |-  ( ph -> B e. V )
32 31 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> B e. V )
33 3 6 16 19 32 grplidd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( 0g ` R ) .+ B ) = B )
34 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
35 34 26 1 4 subrgply1 
 |-  ( S e. ( SubRing ` R ) -> U e. ( SubRing ` ( Poly1 ` R ) ) )
36 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
37 36 subrgss 
 |-  ( U e. ( SubRing ` ( Poly1 ` R ) ) -> U C_ ( Base ` ( Poly1 ` R ) ) )
38 12 35 37 3syl 
 |-  ( ph -> U C_ ( Base ` ( Poly1 ` R ) ) )
39 38 13 sseldd 
 |-  ( ph -> F e. ( Base ` ( Poly1 ` R ) ) )
40 39 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> F e. ( Base ` ( Poly1 ` R ) ) )
41 1nn0 
 |-  1 e. NN0
42 41 a1i 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> 1 e. NN0 )
43 8 34 36 deg1xrcl 
 |-  ( F e. ( Base ` ( Poly1 ` R ) ) -> ( D ` F ) e. RR* )
44 39 43 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
45 44 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( D ` F ) e. RR* )
46 0xr 
 |-  0 e. RR*
47 46 a1i 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> 0 e. RR* )
48 1xr 
 |-  1 e. RR*
49 48 a1i 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> 1 e. RR* )
50 simpr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( D ` F ) <_ 0 )
51 0lt1 
 |-  0 < 1
52 51 a1i 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> 0 < 1 )
53 45 47 49 50 52 xrlelttrd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( D ` F ) < 1 )
54 8 34 36 16 7 deg1lt 
 |-  ( ( F e. ( Base ` ( Poly1 ` R ) ) /\ 1 e. NN0 /\ ( D ` F ) < 1 ) -> ( C ` 1 ) = ( 0g ` R ) )
55 40 42 53 54 syl3anc 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( C ` 1 ) = ( 0g ` R ) )
56 9 55 eqtrid 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> A = ( 0g ` R ) )
57 56 oveq1d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( A .x. X ) = ( ( 0g ` R ) .x. X ) )
58 15 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> X e. V )
59 3 5 16 18 58 ringlzd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( 0g ` R ) .x. X ) = ( 0g ` R ) )
60 57 59 eqtrd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( A .x. X ) = ( 0g ` R ) )
61 60 oveq1d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( A .x. X ) .+ B ) = ( ( 0g ` R ) .+ B ) )
62 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
63 8 34 36 62 deg1le0 
 |-  ( ( R e. Ring /\ F e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( D ` F ) <_ 0 <-> F = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` F ) ` 0 ) ) ) )
64 63 biimpa 
 |-  ( ( ( R e. Ring /\ F e. ( Base ` ( Poly1 ` R ) ) ) /\ ( D ` F ) <_ 0 ) -> F = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` F ) ` 0 ) ) )
65 18 40 50 64 syl21anc 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> F = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` F ) ` 0 ) ) )
66 7 fveq1i 
 |-  ( C ` 0 ) = ( ( coe1 ` F ) ` 0 )
67 10 66 eqtri 
 |-  B = ( ( coe1 ` F ) ` 0 )
68 67 fveq2i 
 |-  ( ( algSc ` ( Poly1 ` R ) ) ` B ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` F ) ` 0 ) )
69 65 68 eqtr4di 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> F = ( ( algSc ` ( Poly1 ` R ) ) ` B ) )
70 69 fveq2d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( Q ` F ) = ( Q ` ( ( algSc ` ( Poly1 ` R ) ) ` B ) ) )
71 70 fveq1d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( Q ` F ) ` X ) = ( ( Q ` ( ( algSc ` ( Poly1 ` R ) ) ` B ) ) ` X ) )
72 12 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> S e. ( SubRing ` R ) )
73 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
74 34 62 26 1 72 73 subrg1ascl 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( algSc ` P ) = ( ( algSc ` ( Poly1 ` R ) ) |` S ) )
75 74 fveq1d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( algSc ` P ) ` B ) = ( ( ( algSc ` ( Poly1 ` R ) ) |` S ) ` B ) )
76 30 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> B e. S )
77 76 fvresd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( ( algSc ` ( Poly1 ` R ) ) |` S ) ` B ) = ( ( algSc ` ( Poly1 ` R ) ) ` B ) )
78 75 77 eqtr2d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( algSc ` ( Poly1 ` R ) ) ` B ) = ( ( algSc ` P ) ` B ) )
79 78 fveq2d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( Q ` ( ( algSc ` ( Poly1 ` R ) ) ` B ) ) = ( Q ` ( ( algSc ` P ) ` B ) ) )
80 79 fveq1d 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( Q ` ( ( algSc ` ( Poly1 ` R ) ) ` B ) ) ` X ) = ( ( Q ` ( ( algSc ` P ) ` B ) ) ` X ) )
81 11 adantr 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> R e. CRing )
82 2 1 26 3 73 81 72 76 58 evls1scafv 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( Q ` ( ( algSc ` P ) ` B ) ) ` X ) = B )
83 71 80 82 3eqtrd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( Q ` F ) ` X ) = B )
84 33 61 83 3eqtr4rd 
 |-  ( ( ph /\ ( D ` F ) <_ 0 ) -> ( ( Q ` F ) ` X ) = ( ( A .x. X ) .+ B ) )
85 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
86 2 3 1 26 4 85 11 12 ressply1evl 
 |-  ( ph -> Q = ( ( eval1 ` R ) |` U ) )
87 86 fveq1d 
 |-  ( ph -> ( Q ` F ) = ( ( ( eval1 ` R ) |` U ) ` F ) )
88 13 fvresd 
 |-  ( ph -> ( ( ( eval1 ` R ) |` U ) ` F ) = ( ( eval1 ` R ) ` F ) )
89 87 88 eqtrd 
 |-  ( ph -> ( Q ` F ) = ( ( eval1 ` R ) ` F ) )
90 89 fveq1d 
 |-  ( ph -> ( ( Q ` F ) ` X ) = ( ( ( eval1 ` R ) ` F ) ` X ) )
91 90 adantr 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> ( ( Q ` F ) ` X ) = ( ( ( eval1 ` R ) ` F ) ` X ) )
92 11 adantr 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> R e. CRing )
93 39 adantr 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> F e. ( Base ` ( Poly1 ` R ) ) )
94 simpr 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> ( D ` F ) = 1 )
95 15 adantr 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> X e. V )
96 34 85 3 36 5 6 7 8 9 10 92 93 94 95 evl1deg1 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> ( ( ( eval1 ` R ) ` F ) ` X ) = ( ( A .x. X ) .+ B ) )
97 91 96 eqtrd 
 |-  ( ( ph /\ ( D ` F ) = 1 ) -> ( ( Q ` F ) ` X ) = ( ( A .x. X ) .+ B ) )
98 8 34 36 39 14 deg1le1 
 |-  ( ph -> ( ( D ` F ) <_ 0 \/ ( D ` F ) = 1 ) )
99 84 97 98 mpjaodan 
 |-  ( ph -> ( ( Q ` F ) ` X ) = ( ( A .x. X ) .+ B ) )