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 ⊢φ→IselectVarsR=j∈𝒫I⟼f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡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∈BaseimPolyr⟼⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x
4 3 a1i ⊢φ→selectVars=i∈V,r∈V⟼j∈𝒫i⟼f∈BaseimPolyr⟼⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x
5 pweq ⊢i=I→𝒫i=𝒫I
6 5 adantr ⊢i=I∧r=R→𝒫i=𝒫I
7 oveq12 ⊢i=I∧r=R→imPolyr=ImPolyR
8 7 fveq2d ⊢i=I∧r=R→BaseimPolyr=BaseImPolyR
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∖jmPolyr=I∖jmPolyR
13 oveq1 ⊢i=I→ievalSubt=IevalSubt
14 13 adantr ⊢i=I∧r=R→ievalSubt=IevalSubt
15 14 fveq1d ⊢i=I∧r=R→ievalSubt⁡ran⁡d=IevalSubt⁡ran⁡d
16 15 fveq1d ⊢i=I∧r=R→ievalSubt⁡ran⁡d⁡d∘f=IevalSubt⁡ran⁡d⁡d∘f
17 simpl ⊢i=I∧r=R→i=I
18 10 11 oveq12d ⊢i=I∧r=R→i∖jmVarr=I∖jmVarR
19 18 fveq1d ⊢i=I∧r=R→i∖jmVarr⁡x=I∖jmVarR⁡x
20 19 fveq2d ⊢i=I∧r=R→c⁡i∖jmVarr⁡x=c⁡I∖jmVarR⁡x
21 20 ifeq2d ⊢i=I∧r=R→ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
22 17 21 mpteq12dv ⊢i=I∧r=R→x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
23 16 22 fveq12d ⊢i=I∧r=R→ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
24 23 csbeq2dv ⊢i=I∧r=R→⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
25 24 csbeq2dv ⊢i=I∧r=R→⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
26 25 csbeq2dv ⊢i=I∧r=R→⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
27 12 26 csbeq12dv ⊢i=I∧r=R→⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
28 8 27 mpteq12dv ⊢i=I∧r=R→f∈BaseimPolyr⟼⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
29 6 28 mpteq12dv ⊢i=I∧r=R→j∈𝒫i⟼f∈BaseimPolyr⟼⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=j∈𝒫I⟼f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
30 29 adantl ⊢φ∧i=I∧r=R→j∈𝒫i⟼f∈BaseimPolyr⟼⦋i∖jmPolyr/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌ievalSubt⁡ran⁡d⁡d∘f⁡x∈i⟼ifx∈jjmVaru⁡xc⁡i∖jmVarr⁡x=j∈𝒫I⟼f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x
31 1 elexd ⊢φ→I∈V
32 2 elexd ⊢φ→R∈V
33 1 pwexd ⊢φ→𝒫I∈V
34 33 mptexd ⊢φ→j∈𝒫I⟼f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x∈V
35 4 30 31 32 34 ovmpod ⊢φ→IselectVarsR=j∈𝒫I⟼f∈BaseImPolyR⟼⦋I∖jmPolyR/u⦌⦋jmPolyu/t⦌⦋algSc⁡t/c⦌⦋c∘algSc⁡u/d⦌IevalSubt⁡ran⁡d⁡d∘f⁡x∈I⟼ifx∈jjmVaru⁡xc⁡I∖jmVarR⁡x