Metamath Proof Explorer


Theorem selvval2

Description: Value of the "variable selection" function. Convert selvval into a simpler form by using evlsevl . (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses selvval2.p P = I mPoly R
selvval2.b B = Base P
selvval2.u U = I J mPoly R
selvval2.t T = J mPoly U
selvval2.c C = algSc T
selvval2.d D = C algSc U
selvval2.r φ R CRing
selvval2.j φ J I
selvval2.f φ F B
Assertion selvval2 φ I selectVars R J F = I eval T D F x I if x J J mVar U x C I J mVar R x

Proof

Step Hyp Ref Expression
1 selvval2.p P = I mPoly R
2 selvval2.b B = Base P
3 selvval2.u U = I J mPoly R
4 selvval2.t T = J mPoly U
5 selvval2.c C = algSc T
6 selvval2.d D = C algSc U
7 selvval2.r φ R CRing
8 selvval2.j φ J I
9 selvval2.f φ F B
10 1 2 3 4 5 6 8 9 selvval φ I selectVars R J F = I evalSub T ran D D F x I if x J J mVar U x C I J mVar R x
11 eqid I evalSub T ran D = I evalSub T ran D
12 eqid I eval T = I eval T
13 eqid I mPoly T 𝑠 ran D = I mPoly T 𝑠 ran D
14 eqid T 𝑠 ran D = T 𝑠 ran D
15 eqid Base I mPoly T 𝑠 ran D = Base I mPoly T 𝑠 ran D
16 1 2 mplrcl F B I V
17 9 16 syl φ I V
18 17 8 ssexd φ J V
19 17 difexd φ I J V
20 3 19 7 mplcrngd φ U CRing
21 4 18 20 mplcrngd φ T CRing
22 3 4 5 6 19 18 7 selvcllem3 φ ran D SubRing T
23 1 2 3 4 5 6 14 13 15 7 8 9 selvcllem4 φ D F Base I mPoly T 𝑠 ran D
24 11 12 13 14 15 17 21 22 23 evlsevl φ I evalSub T ran D D F = I eval T D F
25 24 fveq1d φ I evalSub T ran D D F x I if x J J mVar U x C I J mVar R x = I eval T D F x I if x J J mVar U x C I J mVar R x
26 10 25 eqtrd φ I selectVars R J F = I eval T D F x I if x J J mVar U x C I J mVar R x