Metamath Proof Explorer


Theorem evls1fval

Description: Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019)

Ref Expression
Hypotheses evls1fval.q Q = S evalSub 1 R
evls1fval.e E = 1 𝑜 evalSub S
evls1fval.b B = Base S
Assertion evls1fval S V R 𝒫 B Q = x B B 1 𝑜 x y B 1 𝑜 × y E R

Proof

Step Hyp Ref Expression
1 evls1fval.q Q = S evalSub 1 R
2 evls1fval.e E = 1 𝑜 evalSub S
3 evls1fval.b B = Base S
4 elex S V S V
5 4 adantr S V R 𝒫 B S V
6 simpr S V R 𝒫 B R 𝒫 B
7 ovex B B 1 𝑜 V
8 7 mptex x B B 1 𝑜 x y B 1 𝑜 × y V
9 fvex E R V
10 8 9 coex x B B 1 𝑜 x y B 1 𝑜 × y E R V
11 10 a1i S V R 𝒫 B x B B 1 𝑜 x y B 1 𝑜 × y E R V
12 fveq2 s = S Base s = Base S
13 12 adantr s = S r = R Base s = Base S
14 13 3 syl6eqr s = S r = R Base s = B
15 14 csbeq1d s = S r = R Base s / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r = B / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r
16 3 fvexi B V
17 16 a1i s = S r = R B V
18 id b = B b = B
19 oveq1 b = B b 1 𝑜 = B 1 𝑜
20 18 19 oveq12d b = B b b 1 𝑜 = B B 1 𝑜
21 mpteq1 b = B y b 1 𝑜 × y = y B 1 𝑜 × y
22 21 coeq2d b = B x y b 1 𝑜 × y = x y B 1 𝑜 × y
23 20 22 mpteq12dv b = B x b b 1 𝑜 x y b 1 𝑜 × y = x B B 1 𝑜 x y B 1 𝑜 × y
24 23 coeq1d b = B x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r = x B B 1 𝑜 x y B 1 𝑜 × y 1 𝑜 evalSub s r
25 24 adantl s = S r = R b = B x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r = x B B 1 𝑜 x y B 1 𝑜 × y 1 𝑜 evalSub s r
26 17 25 csbied s = S r = R B / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r = x B B 1 𝑜 x y B 1 𝑜 × y 1 𝑜 evalSub s r
27 oveq2 s = S 1 𝑜 evalSub s = 1 𝑜 evalSub S
28 27 2 syl6eqr s = S 1 𝑜 evalSub s = E
29 28 adantr s = S r = R 1 𝑜 evalSub s = E
30 simpr s = S r = R r = R
31 29 30 fveq12d s = S r = R 1 𝑜 evalSub s r = E R
32 31 coeq2d s = S r = R x B B 1 𝑜 x y B 1 𝑜 × y 1 𝑜 evalSub s r = x B B 1 𝑜 x y B 1 𝑜 × y E R
33 15 26 32 3eqtrd s = S r = R Base s / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r = x B B 1 𝑜 x y B 1 𝑜 × y E R
34 12 3 syl6eqr s = S Base s = B
35 34 pweqd s = S 𝒫 Base s = 𝒫 B
36 df-evls1 evalSub 1 = s V , r 𝒫 Base s Base s / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 evalSub s r
37 33 35 36 ovmpox S V R 𝒫 B x B B 1 𝑜 x y B 1 𝑜 × y E R V S evalSub 1 R = x B B 1 𝑜 x y B 1 𝑜 × y E R
38 5 6 11 37 syl3anc S V R 𝒫 B S evalSub 1 R = x B B 1 𝑜 x y B 1 𝑜 × y E R
39 1 38 syl5eq S V R 𝒫 B Q = x B B 1 𝑜 x y B 1 𝑜 × y E R