Metamath Proof Explorer

Theorem selvffval

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

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

Proof

Step Hyp Ref Expression
1 selvffval.i ⊢ φ → I ∈ V
2 selvffval.r ⊢ φ → R ∈ W
3 df-selv ⊢ selectVars = i ∈ V , r ∈ V ⟼ 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
4 3 a1i ⊢ φ → selectVars = i ∈ V , r ∈ V ⟼ 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 pweq ⊢ i = I → 𝒫 i = 𝒫 I
6 5 adantr ⊢ i = I ∧ r = R → 𝒫 i = 𝒫 I
7 oveq12 ⊢ i = I ∧ r = R → i mPoly r = I mPoly R
8 7 fveq2d ⊢ i = I ∧ r = R → Base i mPoly r = Base I mPoly R
9 difeq1 ⊢ i = I → i ∖ j = I ∖ j
10 9 adantr ⊢ i = I ∧ r = R → i ∖ j = I ∖ j
11 simpr ⊢ i = I ∧ r = R → r = R
12 10 11 oveq12d ⊢ i = I ∧ r = R → i ∖ j mPoly r = I ∖ j mPoly R
13 oveq1 ⊢ i = I → i evalSub t = I evalSub t
14 13 adantr ⊢ i = I ∧ r = R → i evalSub t = I evalSub t
15 14 fveq1d ⊢ i = I ∧ r = R → i evalSub t ⁡ ran ⁡ d = I evalSub t ⁡ ran ⁡ d
16 15 fveq1d ⊢ i = I ∧ r = R → i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f
17 simpl ⊢ i = I ∧ r = R → i = I
18 10 11 oveq12d ⊢ i = I ∧ r = R → i ∖ j mVar r = I ∖ j mVar R
19 18 fveq1d ⊢ i = I ∧ r = R → i ∖ j mVar r ⁡ x = I ∖ j mVar R ⁡ x
20 19 fveq2d ⊢ i = I ∧ r = R → c ⁡ i ∖ j mVar r ⁡ x = c ⁡ I ∖ j mVar R ⁡ x
21 20 ifeq2d ⊢ i = I ∧ r = R → 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
22 17 21 mpteq12dv ⊢ i = I ∧ r = R → 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
23 16 22 fveq12d ⊢ i = I ∧ r = R → 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
24 23 csbeq2dv ⊢ i = I ∧ r = R → ⦋ 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
25 24 csbeq2dv ⊢ i = I ∧ r = R → ⦋ 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
26 25 csbeq2dv ⊢ i = I ∧ r = 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 = ⦋ 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
27 12 26 csbeq12dv ⊢ i = I ∧ r = 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 = ⦋ 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
28 8 27 mpteq12dv ⊢ i = I ∧ r = R → 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
29 6 28 mpteq12dv ⊢ i = I ∧ r = 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 = 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
30 29 adantl ⊢ φ ∧ i = I ∧ r = 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 = 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
31 1 elexd ⊢ φ → I ∈ V
32 2 elexd ⊢ φ → R ∈ V
33 1 pwexd ⊢ φ → 𝒫 I ∈ V
34 33 mptexd ⊢ φ → 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 ∈ V
35 4 30 31 32 34 ovmpod ⊢ φ → 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