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 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1fval.e 𝐸 = ( 1o evalSub 𝑆 )
evls1fval.b 𝐵 = ( Base ‘ 𝑆 )
Assertion evls1fval ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 evls1fval.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1fval.e 𝐸 = ( 1o evalSub 𝑆 )
3 evls1fval.b 𝐵 = ( Base ‘ 𝑆 )
4 elex ( 𝑆𝑉𝑆 ∈ V )
5 4 adantr ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → 𝑆 ∈ V )
6 simpr ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → 𝑅 ∈ 𝒫 𝐵 )
7 ovex ( 𝐵m ( 𝐵m 1o ) ) ∈ V
8 7 mptex ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ V
9 fvex ( 𝐸𝑅 ) ∈ V
10 8 9 coex ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ∈ V
11 10 a1i ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ∈ V )
12 fveq2 ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
13 12 adantr ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
14 13 3 syl6eqr ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( Base ‘ 𝑠 ) = 𝐵 )
15 14 csbeq1d ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( Base ‘ 𝑠 ) / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = 𝐵 / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
16 3 fvexi 𝐵 ∈ V
17 16 a1i ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → 𝐵 ∈ V )
18 id ( 𝑏 = 𝐵𝑏 = 𝐵 )
19 oveq1 ( 𝑏 = 𝐵 → ( 𝑏m 1o ) = ( 𝐵m 1o ) )
20 18 19 oveq12d ( 𝑏 = 𝐵 → ( 𝑏m ( 𝑏m 1o ) ) = ( 𝐵m ( 𝐵m 1o ) ) )
21 mpteq1 ( 𝑏 = 𝐵 → ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) )
22 21 coeq2d ( 𝑏 = 𝐵 → ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
23 20 22 mpteq12dv ( 𝑏 = 𝐵 → ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
24 23 coeq1d ( 𝑏 = 𝐵 → ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
25 24 adantl ( ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
26 17 25 csbied ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → 𝐵 / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
27 oveq2 ( 𝑠 = 𝑆 → ( 1o evalSub 𝑠 ) = ( 1o evalSub 𝑆 ) )
28 27 2 syl6eqr ( 𝑠 = 𝑆 → ( 1o evalSub 𝑠 ) = 𝐸 )
29 28 adantr ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( 1o evalSub 𝑠 ) = 𝐸 )
30 simpr ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
31 29 30 fveq12d ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) = ( 𝐸𝑅 ) )
32 31 coeq2d ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
33 15 26 32 3eqtrd ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( Base ‘ 𝑠 ) / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
34 12 3 syl6eqr ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝐵 )
35 34 pweqd ( 𝑠 = 𝑆 → 𝒫 ( Base ‘ 𝑠 ) = 𝒫 𝐵 )
36 df-evls1 evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ( Base ‘ 𝑠 ) / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
37 33 35 36 ovmpox ( ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 𝐵 ∧ ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ∈ V ) → ( 𝑆 evalSub1 𝑅 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
38 5 6 11 37 syl3anc ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → ( 𝑆 evalSub1 𝑅 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
39 1 38 syl5eq ( ( 𝑆𝑉𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )