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 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 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 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( 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 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( 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 × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) )