Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evls1fval Structured version   Visualization version   GIF version

Theorem evls1fval 20984
 Description: Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.)
Hypotheses
Ref Expression
evls1fval.q 𝑄 = (𝑆 evalSub1 𝑅)
evls1fval.e 𝐸 = (1o evalSub 𝑆)
evls1fval.b 𝐵 = (Base‘𝑆)
Assertion
Ref Expression
evls1fval ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
Distinct variable group:   𝑥,𝐵,𝑦
Allowed substitution hints:   𝑄(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem evls1fval
Dummy variables 𝑏 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evls1fval.q . 2 𝑄 = (𝑆 evalSub1 𝑅)
2 elex 3460 . . . 4 (𝑆𝑉𝑆 ∈ V)
32adantr 484 . . 3 ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → 𝑆 ∈ V)
4 simpr 488 . . 3 ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → 𝑅 ∈ 𝒫 𝐵)
5 ovex 7178 . . . . . 6 (𝐵m (𝐵m 1o)) ∈ V
65mptex 6973 . . . . 5 (𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∈ V
7 fvex 6668 . . . . 5 (𝐸𝑅) ∈ V
86, 7coex 7630 . . . 4 ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)) ∈ V
98a1i 11 . . 3 ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)) ∈ V)
10 fveq2 6655 . . . . . . . 8 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
1110adantr 484 . . . . . . 7 ((𝑠 = 𝑆𝑟 = 𝑅) → (Base‘𝑠) = (Base‘𝑆))
12 evls1fval.b . . . . . . 7 𝐵 = (Base‘𝑆)
1311, 12eqtr4di 2851 . . . . . 6 ((𝑠 = 𝑆𝑟 = 𝑅) → (Base‘𝑠) = 𝐵)
1413csbeq1d 3834 . . . . 5 ((𝑠 = 𝑆𝑟 = 𝑅) → (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = 𝐵 / 𝑏((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
1512fvexi 6669 . . . . . . 7 𝐵 ∈ V
1615a1i 11 . . . . . 6 ((𝑠 = 𝑆𝑟 = 𝑅) → 𝐵 ∈ V)
17 id 22 . . . . . . . . . 10 (𝑏 = 𝐵𝑏 = 𝐵)
18 oveq1 7152 . . . . . . . . . 10 (𝑏 = 𝐵 → (𝑏m 1o) = (𝐵m 1o))
1917, 18oveq12d 7163 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏m (𝑏m 1o)) = (𝐵m (𝐵m 1o)))
20 mpteq1 5122 . . . . . . . . . 10 (𝑏 = 𝐵 → (𝑦𝑏 ↦ (1o × {𝑦})) = (𝑦𝐵 ↦ (1o × {𝑦})))
2120coeq2d 5701 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦}))) = (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦}))))
2219, 21mpteq12dv 5119 . . . . . . . 8 (𝑏 = 𝐵 → (𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) = (𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))))
2322coeq1d 5700 . . . . . . 7 (𝑏 = 𝐵 → ((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
2423adantl 485 . . . . . 6 (((𝑠 = 𝑆𝑟 = 𝑅) ∧ 𝑏 = 𝐵) → ((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
2516, 24csbied 3866 . . . . 5 ((𝑠 = 𝑆𝑟 = 𝑅) → 𝐵 / 𝑏((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
26 oveq2 7153 . . . . . . . . 9 (𝑠 = 𝑆 → (1o evalSub 𝑠) = (1o evalSub 𝑆))
27 evls1fval.e . . . . . . . . 9 𝐸 = (1o evalSub 𝑆)
2826, 27eqtr4di 2851 . . . . . . . 8 (𝑠 = 𝑆 → (1o evalSub 𝑠) = 𝐸)
2928adantr 484 . . . . . . 7 ((𝑠 = 𝑆𝑟 = 𝑅) → (1o evalSub 𝑠) = 𝐸)
30 simpr 488 . . . . . . 7 ((𝑠 = 𝑆𝑟 = 𝑅) → 𝑟 = 𝑅)
3129, 30fveq12d 6662 . . . . . 6 ((𝑠 = 𝑆𝑟 = 𝑅) → ((1o evalSub 𝑠)‘𝑟) = (𝐸𝑅))
3231coeq2d 5701 . . . . 5 ((𝑠 = 𝑆𝑟 = 𝑅) → ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
3314, 25, 323eqtrd 2837 . . . 4 ((𝑠 = 𝑆𝑟 = 𝑅) → (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
3410, 12eqtr4di 2851 . . . . 5 (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
3534pweqd 4519 . . . 4 (𝑠 = 𝑆 → 𝒫 (Base‘𝑠) = 𝒫 𝐵)
36 df-evls1 20980 . . . 4 evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏m (𝑏m 1o)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
3733, 35, 36ovmpox 7293 . . 3 ((𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 𝐵 ∧ ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)) ∈ V) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
383, 4, 9, 37syl3anc 1368 . 2 ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
391, 38syl5eq 2845 1 ((𝑆𝑉𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵m (𝐵m 1o)) ↦ (𝑥 ∘ (𝑦𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸𝑅)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3442  ⦋csb 3830  𝒫 cpw 4500  {csn 4528   ↦ cmpt 5114   × cxp 5521   ∘ ccom 5527  ‘cfv 6332  (class class class)co 7145  1oc1o 8096   ↑m cmap 8407  Basecbs 16495   evalSub ces 20779   evalSub1 ces1 20978 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-evls1 20980 This theorem is referenced by:  evls1val  20985  evls1rhm  20987  evls1sca  20988  evl1fval1lem  20995
 Copyright terms: Public domain W3C validator