Metamath Proof Explorer

Theorem selvval

Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023)

Ref Expression
Hypotheses selvval.p ⊢ P = I mPoly R
selvval.b ⊢ B = Base P
selvval.u ⊢ U = I ∖ J mPoly R
selvval.t ⊢ T = J mPoly U
selvval.c ⊢ C = algSc ⁡ T
selvval.d ⊢ D = C ∘ algSc ⁡ U
selvval.i ⊢ φ → I ∈ V
selvval.r ⊢ φ → R ∈ W
selvval.j ⊢ φ → J ⊆ I
selvval.f ⊢ φ → F ∈ B
Assertion 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

Proof

Step Hyp Ref Expression
1 selvval.p ⊢ P = I mPoly R
2 selvval.b ⊢ B = Base P
3 selvval.u ⊢ U = I ∖ J mPoly R
4 selvval.t ⊢ T = J mPoly U
5 selvval.c ⊢ C = algSc ⁡ T
6 selvval.d ⊢ D = C ∘ algSc ⁡ U
7 selvval.i ⊢ φ → I ∈ V
8 selvval.r ⊢ φ → R ∈ W
9 selvval.j ⊢ φ → J ⊆ I
10 selvval.f ⊢ φ → F ∈ B
11 7 8 9 selvfval ⊢ φ → I selectVars R ⁡ J = f ∈ Base I mPoly R ⟼ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
12 coeq2 ⊢ f = F → d ∘ f = d ∘ F
13 12 fveq2d ⊢ f = F → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F
14 13 fveq1d ⊢ f = F → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
15 14 csbeq2dv ⊢ f = F → ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
16 15 csbeq2dv ⊢ f = F → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
17 16 csbeq2dv ⊢ f = F → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
18 17 csbeq2dv ⊢ f = F → ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
19 18 adantl ⊢ φ ∧ f = F → ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
20 1 fveq2i ⊢ Base P = Base I mPoly R
21 2 20 eqtri ⊢ B = Base I mPoly R
22 10 21 eleqtrdi ⊢ φ → F ∈ Base I mPoly R
23 fvex ⊢ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
24 23 csbex ⊢ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
25 24 csbex ⊢ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
26 25 csbex ⊢ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
27 26 csbex ⊢ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
28 27 a1i ⊢ φ → ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
29 11 19 22 28 fvmptd ⊢ φ → I selectVars R ⁡ J ⁡ F = ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
30 ovex ⊢ I ∖ J mPoly R ∈ V
31 3 eqeq2i ⊢ u = U ↔ u = I ∖ J mPoly R
32 oveq2 ⊢ u = U → J mPoly u = J mPoly U
33 fveq2 ⊢ u = U → algSc ⁡ u = algSc ⁡ U
34 33 coeq2d ⊢ u = U → c ∘ algSc ⁡ u = c ∘ algSc ⁡ U
35 oveq2 ⊢ u = U → J mVar u = J mVar U
36 35 fveq1d ⊢ u = U → J mVar u ⁡ x = J mVar U ⁡ x
37 36 ifeq1d ⊢ u = U → if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
38 37 mpteq2dv ⊢ u = U → x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
39 38 fveq2d ⊢ u = U → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
40 34 39 csbeq12dv ⊢ u = U → ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
41 40 csbeq2dv ⊢ u = U → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
42 32 41 csbeq12dv ⊢ u = U → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ J mPoly U / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
43 ovex ⊢ J mPoly U ∈ V
44 4 eqeq2i ⊢ t = T ↔ t = J mPoly U
45 fveq2 ⊢ t = T → algSc ⁡ t = algSc ⁡ T
46 oveq2 ⊢ t = T → I evalSub t = I evalSub T
47 46 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d = I evalSub T ⁡ ran ⁡ d
48 47 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F
49 48 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
50 49 csbeq2dv ⊢ t = T → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
51 45 50 csbeq12dv ⊢ t = T → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ T / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
52 fvex ⊢ algSc ⁡ T ∈ V
53 5 eqeq2i ⊢ c = C ↔ c = algSc ⁡ T
54 coeq1 ⊢ c = C → c ∘ algSc ⁡ U = C ∘ algSc ⁡ U
55 fveq1 ⊢ c = C → c ⁡ I ∖ J mVar R ⁡ x = C ⁡ I ∖ J mVar R ⁡ x
56 55 ifeq2d ⊢ c = C → if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
57 56 mpteq2dv ⊢ c = C → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
58 57 fveq2d ⊢ c = C → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
59 54 58 csbeq12dv ⊢ c = C → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ C ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
60 5 fvexi ⊢ C ∈ V
61 fvex ⊢ algSc ⁡ U ∈ V
62 60 61 coex ⊢ C ∘ algSc ⁡ U ∈ V
63 6 eqeq2i ⊢ d = D ↔ d = C ∘ algSc ⁡ U
64 rneq ⊢ d = D → ran ⁡ d = ran ⁡ D
65 64 fveq2d ⊢ d = D → I evalSub T ⁡ ran ⁡ d = I evalSub T ⁡ ran ⁡ D
66 coeq1 ⊢ d = D → d ∘ F = D ∘ F
67 65 66 fveq12d ⊢ d = D → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F
68 67 fveq1d ⊢ d = D → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
69 63 68 sylbir ⊢ d = C ∘ algSc ⁡ U → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
70 62 69 csbie ⊢ ⦋ C ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
71 59 70 eqtrdi ⊢ c = C → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
72 53 71 sylbir ⊢ c = algSc ⁡ T → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
73 52 72 csbie ⊢ ⦋ algSc ⁡ T / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
74 51 73 eqtrdi ⊢ t = T → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
75 44 74 sylbir ⊢ t = J mPoly U → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
76 43 75 csbie ⊢ ⦋ J mPoly U / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
77 42 76 eqtrdi ⊢ u = U → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
78 31 77 sylbir ⊢ u = I ∖ J mPoly R → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
79 30 78 csbie ⊢ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
80 29 79 eqtrdi ⊢ φ → 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