Metamath Proof Explorer

Theorem selvfval

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

Ref Expression
Hypotheses selvffval.i ⊢ φ → I ∈ V
selvffval.r ⊢ φ → R ∈ W
selvfval.j ⊢ φ → J ⊆ I
Assertion 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

Proof

Step Hyp Ref Expression
1 selvffval.i ⊢ φ → I ∈ V
2 selvffval.r ⊢ φ → R ∈ W
3 selvfval.j ⊢ φ → J ⊆ I
4 1 2 selvffval ⊢ φ → I selectVars R = j ∈ 𝒫 I ⟼ 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
5 difeq2 ⊢ j = J → I ∖ j = I ∖ J
6 5 oveq1d ⊢ j = J → I ∖ j mPoly R = I ∖ J mPoly R
7 oveq1 ⊢ j = J → j mPoly u = J mPoly u
8 eleq2 ⊢ j = J → x ∈ j ↔ x ∈ J
9 oveq1 ⊢ j = J → j mVar u = J mVar u
10 9 fveq1d ⊢ j = J → j mVar u ⁡ x = J mVar u ⁡ x
11 5 oveq1d ⊢ j = J → I ∖ j mVar R = I ∖ J mVar R
12 11 fveq1d ⊢ j = J → I ∖ j mVar R ⁡ x = I ∖ J mVar R ⁡ x
13 12 fveq2d ⊢ j = J → c ⁡ I ∖ j mVar R ⁡ x = c ⁡ I ∖ J mVar R ⁡ x
14 8 10 13 ifbieq12d ⊢ j = J → 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
15 14 mpteq2dv ⊢ j = J → 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
16 15 fveq2d ⊢ j = J → 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
17 16 csbeq2dv ⊢ j = J → ⦋ 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
18 17 csbeq2dv ⊢ j = J → ⦋ 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
19 7 18 csbeq12dv ⊢ j = J → ⦋ 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
20 6 19 csbeq12dv ⊢ j = J → ⦋ 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
21 20 mpteq2dv ⊢ j = 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 = 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
22 21 adantl ⊢ φ ∧ j = 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 = 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
23 1 3 sselpwd ⊢ φ → J ∈ 𝒫 I
24 fvex ⊢ Base I mPoly R ∈ V
25 mptexg ⊢ Base I mPoly R ∈ V → 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 ∈ V
26 24 25 mp1i ⊢ φ → 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 ∈ V
27 4 22 23 26 fvmptd ⊢ φ → 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